From ed6a8ab2478838d4a31dfdde6d357060cf8ad66f Mon Sep 17 00:00:00 2001 From: Peter Goodspeed-Niklaus Date: Wed, 22 Jan 2025 09:14:26 +0100 Subject: [PATCH] build: add a retry on `git push` in `merge-pr.sh` Github sometimes takes a few seconds to figure out that after a force-push to a branch, we are still allowed to merge it to main. So this does a sleep/retry, once, in the event that the first push fails. --- scripts/merge-pr.sh | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/scripts/merge-pr.sh b/scripts/merge-pr.sh index 11e9facbc5..51f4f0c8e7 100755 --- a/scripts/merge-pr.sh +++ b/scripts/merge-pr.sh @@ -65,4 +65,13 @@ fi # we can now actually merge this to main without breaking anything git checkout main git merge "$branch" --ff-only -git push + +# In principle we can just push now, because we're just updating `main` to the tip of an approved branch. +# Github has magic to detect that! +# Unfortunately, the magic is sometimes laggy. +# So let's give it a shot, and if it doesn't work, we'll try again a few seconds later; +# that should minimize overall waiting. +if ! git push; then + sleep 2.5s + git push +fi