diff --git a/jenkins-build-all b/jenkins-build-all index a1ee7c11..2abac58c 100755 --- a/jenkins-build-all +++ b/jenkins-build-all @@ -65,7 +65,7 @@ cd $WORKSPACE # this can be handled in the jenkins job, or here: if [ -e fdroiddata ]; then cd fdroiddata - git remote update -p + while ! git fetch origin --tags --prune; do sleep 10; done git checkout master git reset --hard origin/master # keep all the cloned source repos diff --git a/jenkins-setup-build-environment b/jenkins-setup-build-environment index abe123bd..a7829c6f 100755 --- a/jenkins-setup-build-environment +++ b/jenkins-setup-build-environment @@ -68,7 +68,7 @@ fi # this can be handled in the jenkins job, or here: if [ -e fdroiddata ]; then cd fdroiddata - while ! git fetch; do sleep 1; done + while ! git fetch origin --tags --prune; do sleep 10; done git remote update -p git checkout master git reset --hard origin/master