diff options
Diffstat (limited to 'scripts/push-repo-mirrors.bash')
| -rw-r--r-- | scripts/push-repo-mirrors.bash | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/scripts/push-repo-mirrors.bash b/scripts/push-repo-mirrors.bash index bc0ac1e..5058134 100644 --- a/scripts/push-repo-mirrors.bash +++ b/scripts/push-repo-mirrors.bash @@ -48,6 +48,21 @@ for repository in /repositories/*; do GITHUB_TOKEN=$(cat /run/secrets/github_token) mirror_host="${mirror#https://}" + + # Update the GitHub repo's default branch to match the local HEAD before mirroring, + # so that --mirror can delete any branch that was previously the default. + local_default=$(git symbolic-ref --short HEAD 2>/dev/null) + github_repo="${mirror#https://github.com/}" + if [ -n "$local_default" ]; then + echo "Setting GitHub default branch to '$local_default' for $github_repo" + curl -sf -X PATCH \ + -H "Authorization: Bearer $GITHUB_TOKEN" \ + -H "Accept: application/vnd.github+json" \ + -d "{\"default_branch\":\"$local_default\"}" \ + "https://api.github.com/repos/$github_repo" > /dev/null \ + || echo "Warning: failed to update default branch on GitHub for $github_repo" + fi + echo "Pushing to GitHub mirror: $mirror" git push --mirror "https://x-access-token:$GITHUB_TOKEN@$mirror_host" 2>&1 | sed "s/$GITHUB_TOKEN/[REDACTED]/g" || echo "Failed to push to $mirror" ;; |