CI: retry pushing 10 times to nightly

This commit is contained in:
Frank Morgner 2019-10-18 00:41:10 +02:00
parent 8ded1ae94b
commit 01678e871e
1 changed files with 5 additions and 4 deletions

View File

@ -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