diff options
| author | Maxim Kuvyrkov <maxim.kuvyrkov@linaro.org> | 2018-01-22 17:26:14 +0000 |
|---|---|---|
| committer | Maxim Kuvyrkov <maxim.kuvyrkov@linaro.org> | 2018-01-22 17:26:14 +0000 |
| commit | a41dbfd084c5aa72ec31776311e698daf468c855 (patch) | |
| tree | 1fd3afc7c0e7c12c16e13e7928de3a9ba67a76b2 /jenkins-helpers.sh | |
| parent | d3817e7a8ea65dbd5ba5bcb11b6ced091487e6e7 (diff) | |
jenkins-helpers.sh: Add optional reference repo param to clone_or_update_repo
Change-Id: I64292cb36fac6bc5afcb68dc5f8b90236d0ac26a
Diffstat (limited to 'jenkins-helpers.sh')
| -rw-r--r-- | jenkins-helpers.sh | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/jenkins-helpers.sh b/jenkins-helpers.sh index 1db7a6a1..8b6f6197 100644 --- a/jenkins-helpers.sh +++ b/jenkins-helpers.sh @@ -161,6 +161,7 @@ remote_exec () # $1 -- repo directory # $2 -- branch, tag or refspec # $3 -- master git repo +# $4 -- reference git repo (to speedup initial cloning) clone_or_update_repo () { ( @@ -169,10 +170,15 @@ clone_or_update_repo () local dir="$1" local ref="$2" local url="$3" + local refrepo="$4" if ! [ -d "$dir/.git" ]; then rm -rf "$dir" - git clone "$url" "$dir" + refopt="" + if [ "$refrepo" != "" ]; then + refopt="--reference $refrepo" + fi + git clone $refopt "$url" "$dir" fi ( |