Retry git pushes

Can happen that they fail in case a PR got merged meanwhile
NixOS · Sep 17, 2024 · 35cdd2f · 35cdd2f
1 parent b0e7489
commit 35cdd2f
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 2 deletions.
diff --git a/scripts/endorse.sh b/scripts/endorse.sh
@@ -46,7 +46,9 @@ EOF
 echo "$ENDORSER_ID" >> "$endorsersAskedFile"
 git add "$endorsersAskedFile"
 git commit -m "Update list of endorsers asked"
-git push
+while ! git push; do
+  git pull --rebase
+done
 
 gh api \
   --method POST \

diff --git a/scripts/update-voter-team.sh b/scripts/update-voter-team.sh
@@ -116,5 +116,7 @@ done | sort > "$invitedFile"
 git add scripts/invited.txt
 if ! git diff --cached --exit-code; then
   git commit -m "Update list of invited users"
-  git push
+  while ! git push; do
+    git pull --rebase
+  done
 fi