ci: move scripts into separate directory
authorPetr Štetiar <ynezz@true.cz>
Mon, 5 Sep 2022 07:04:27 +0000 (09:04 +0200)
committerChristian Marangi <ansuelsmth@gmail.com>
Sun, 4 Dec 2022 16:36:54 +0000 (17:36 +0100)
commitf2fb3ffd712dd35eca1f979c6852c6ccf7a88333
tree740ad39a89fdf915b5336105845e35a6fc914f68
parent7ff1477b3d8ea92c4061a6b8a7f3af6f35c0ca4a
ci: move scripts into separate directory

So it's clean and tidy.

Signed-off-by: Petr Štetiar <ynezz@true.cz>
(cherry picked from commit 63ed733d30153667d7d645ab0ee3f5614089c759)
.github/workflows/ci_helpers.sh [deleted file]
.github/workflows/formal.yml
.github/workflows/scripts/ci_helpers.sh [new file with mode: 0644]