From 84dc4158371c0e0a9af9ee642800b3ee5a057543 Mon Sep 17 00:00:00 2001
From: Hans-Christoph Steiner <hans@eds.org>
Date: Wed, 26 Oct 2016 14:24:14 +0200
Subject: [PATCH] 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.
---
 jenkins-build-makebuildserver | 1 +
 1 file changed, 1 insertion(+)

diff --git a/jenkins-build-makebuildserver b/jenkins-build-makebuildserver
index 6d459fa5..b3877f59 100755
--- 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
-- 
2.30.2