diff options
author | Maxim Kuvyrkov <maxim.kuvyrkov@linaro.org> | 2017-05-17 13:47:47 +0000 |
---|---|---|
committer | Maxim Kuvyrkov <maxim.kuvyrkov@linaro.org> | 2017-05-18 12:22:12 +0000 |
commit | 59a1f2a72531d68e542884da16cea7789b4a7c24 (patch) | |
tree | a7ae59bd83d6702fb3cfe1c5c797c97a57bbfa70 | |
parent | 04e46bf98e001cd67155b5a3eef40d0e788127d9 (diff) |
jenkins-helpers.sh: New helper to clone/update repos.
Change-Id: I7f70eb448df590db2e810e2e5bbf8a56b18911fe
-rw-r--r-- | jenkins-helpers.sh | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/jenkins-helpers.sh b/jenkins-helpers.sh index 58c120ed..363afa33 100644 --- a/jenkins-helpers.sh +++ b/jenkins-helpers.sh @@ -123,3 +123,36 @@ remote_exec () for i in "$@"; do cmd+=($(printf '%q' "$i")); done ssh ${port:+-p$port} $host "${dir:+cd "$(printf '%q' "$dir")" &&} exec ${cmd[@]}" } + +# Clone or update a git repo +# $1 -- repo directory +# $2 -- branch, tag or refspec +# $3 -- master git repo +clone_or_update_repo () +{ + local dir="$1" + local ref="$2" + local url="$3" + + if ! [ -d "$dir/.git" ]; then + rm -rf "$dir" + git clone "$url" "$dir" + fi + + ( + cd "$dir" + + # Convert git branch/tag names into SHA1 + local sha1 + sha1=$(git ls-remote "$url" "$ref" | cut -f 1) + + # Update from URL. + git remote set-url origin "$url" + git remote update -p + + # Checkout + git reset --hard + git clean -dfx + git checkout --detach "$sha1" + ) +} |