Merge pull request #6425 from cgundogan/pr/jenkins_git_fetch_timeout

jenkins: timeout and retry blocked git fetch
RIOT-OS · Jan 19, 2017 · f072bce · f072bce
2 parents 8ba057d + b523808
commit f072bce
Showing 1 changed file with 7 additions and 3 deletions.
diff --git a/Jenkinsfile b/Jenkinsfile
@@ -218,7 +218,11 @@ def abortOnError(msg)
 
 def fetchPR(prNum, fetchArgs, extraRefSpec)
 {
-    sh """git init; git remote add origin https://github.com/RIOT-OS/RIOT;
-    git fetch -u -n ${fetchArgs} origin ${extraRefSpec} pull/${prNum}/merge:pull_${prNum}
-    git checkout pull_${prNum}"""
+    retry(3) {
+        timeout(time: 60, unit: 'SECONDS') {
+            sh """git init; git remote add origin https://github.com/RIOT-OS/RIOT;
+            git fetch -u -n ${fetchArgs} origin ${extraRefSpec} pull/${prNum}/merge:pull_${prNum}
+            git checkout pull_${prNum}"""
+        }
+    }
 }