From 74067bebed5d152804417678ef9b90ca8542a6d1 Mon Sep 17 00:00:00 2001 From: Stephen Gutekanst Date: Sat, 24 Jun 2023 19:07:43 -0700 Subject: [PATCH] dev: remove directory Signed-off-by: Stephen Gutekanst --- {dev => .github}/push-subrepos.sh | 0 .github/workflows/push_subrepos.yml | 2 +- 2 files changed, 1 insertion(+), 1 deletion(-) rename {dev => .github}/push-subrepos.sh (100%) diff --git a/dev/push-subrepos.sh b/.github/push-subrepos.sh similarity index 100% rename from dev/push-subrepos.sh rename to .github/push-subrepos.sh diff --git a/.github/workflows/push_subrepos.yml b/.github/workflows/push_subrepos.yml index f579f58a..b1f8fbfd 100644 --- a/.github/workflows/push_subrepos.yml +++ b/.github/workflows/push_subrepos.yml @@ -25,4 +25,4 @@ jobs: git config user.email 'stephen@hexops.com' # See https://github.community/t/automating-push-to-public-repo/17742/12 git config -l | grep 'http\..*\.extraheader' | cut -d= -f1 | xargs -L1 git config --unset-all - ./dev/push-subrepos.sh + ./.github/push-subrepos.sh