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