jenkins-build-makebuildserver: retry `git fetch` until it works

It seems that gitlab gives 500 errors a bit too frequently, so keep
retrying the `git pull` until it works so that there isn't a error email
sent out over failed pulls.

diff --git a/jenkins-build-makebuildserver b/jenkins-build-makebuildserver
index 6d459fa5722bb916cb677bb454ab3ed8899e2470..b3877f5903ede53528c1664eb82c6c0600b5e9aa 100755 (executable)
--- a/jenkins-build-makebuildserver
+++ b/jenkins-build-makebuildserver
@@ -54,6 +54,7 @@ echo "apt_package_cache = True" >> $WORKSPACE/makebuildserver.config.py
 # this can be handled in the jenkins job, or here:
 if [ -e fdroiddata ]; then
     cd fdroiddata
+    while ! git fetch; do sleep 1; done
     git remote update -p
     git checkout master
     git reset --hard origin/master