riot-ci/RIOT
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

jenkins: use local RIOT mirror to speed up fetches

Browse Source
This commit is contained in:
Cenk Gündoğan 2017-01-20 16:08:50 +01:00 committed by Cenk Gündoğan
parent 85d8397464
commit 1e67b7a57c
1 changed files with 6 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
Jenkinsfile vendored
View File

@ -14,6 +14,8 @@ abortPreviousBuilds()
stage('setup') { stage('setup') {
node ('master') { node ('master') {
sh '(( "\${RIOT_MIRROR}" )) && git -C "\${RIOT_MIRROR_DIR}" fetch --all'
deleteDir() deleteDir()
fetchPR(env.CHANGE_ID, "--depth=1", "") fetchPR(env.CHANGE_ID, "--depth=1", "")
@ -220,7 +222,10 @@ def fetchPR(prNum, fetchArgs, extraRefSpec)
{ {
retry(3) { retry(3) {
timeout(time: 60, unit: 'SECONDS') { 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 fetch -u -n ${fetchArgs} origin ${extraRefSpec} pull/${prNum}/merge:pull_${prNum}
git checkout pull_${prNum}""" git checkout pull_${prNum}"""
} }