From 1e67b7a57c24e692b5277d99d2219412f0a2b3e2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cenk=20G=C3=BCndo=C4=9Fan?= <mail-github@cgundogan.de>
Date: Fri, 20 Jan 2017 16:08:50 +0100
Subject: [PATCH] jenkins: use local RIOT mirror to speed up fetches
---
Jenkinsfile | 7 ++++++-
1 file changed, 6 insertions(+), 1 deletion(-)
diff --git a/Jenkinsfile b/Jenkinsfile
index 0820478384..0bf59638bb 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -14,6 +14,8 @@ abortPreviousBuilds()
stage('setup') {
node ('master') {
+ sh '(( "\${RIOT_MIRROR}" )) && git -C "\${RIOT_MIRROR_DIR}" fetch --all'
+
deleteDir()
fetchPR(env.CHANGE_ID, "--depth=1", "")
@@ -220,7 +222,10 @@ def fetchPR(prNum, fetchArgs, extraRefSpec)
{
retry(3) {
timeout(time: 60, unit: 'SECONDS') {
- sh """git init; git remote add origin https://github.com/RIOT-OS/RIOT;
+ deleteDir()
+ sh """git init
+ if (( "\${RIOT_MIRROR}" )); then RIOT_URL="\${RIOT_MIRROR_URL}"; else RIOT_URL="https://github.com/RIOT-OS/RIOT"; fi
+ git remote add origin "\${RIOT_URL}"
git fetch -u -n ${fetchArgs} origin ${extraRefSpec} pull/${prNum}/merge:pull_${prNum}
git checkout pull_${prNum}"""
}
--
GitLab