diff --git a/.github/push_artifacts.sh b/.github/push_artifacts.sh index a4974eb9..15d07868 100755 --- a/.github/push_artifacts.sh +++ b/.github/push_artifacts.sh @@ -19,9 +19,10 @@ do done git commit --message "$1" -if ! git push --quiet --set-upstream origin "${BRANCH}" -then +i=0 +while [ $i -le 10 ] && ! git push --quiet --set-upstream origin "${BRANCH}" +do sleep $[ ( $RANDOM % 32 ) + 1 ]s git pull --rebase origin "${BRANCH}" - git push --quiet --set-upstream origin "${BRANCH}" -fi + i=$(( $i + 1 )) +done