1 files changed, 23 insertions, 6 deletions
diff --git a/jenkins-helpers.sh b/jenkins-helpers.sh
index 7feb3edf..771ace4b 100644
--- a/jenkins-helpers.sh
+++ b/jenkins-helpers.sh
@@ -514,6 +514,28 @@ clone_or_update_repo_no_checkout ()
     )
 }
 
+# Checkout branch/ref/SHA1 in a git repo
+# $1 -- repo directory
+# $2 -- ref to checkout
+# $3 -- name of the git remote
+git_checkout ()
+{
+    (
+    set -euf -o pipefail
+
+    local dir="$1"
+    local ref="$2"
+    local remote="$3"
+
+    git_clean "$dir"
+    # Convert git branch/tag names into SHA1
+    local sha1
+    sha1=$(git_rev_parse "$dir" "$ref" "$remote")
+    # Checkout
+    git -C "$dir" checkout --detach "$sha1"
+    )
+}
+
 # Clone or update a git repo
 # $1 -- repo directory
 # $2 -- ref to checkout
@@ -536,12 +558,7 @@ clone_or_update_repo ()
     clone_or_update_repo_no_checkout "$dir" "$url" "$reference" \
 				     "$single_branch" "$remote"
 
-    git_clean "$dir"
-    # Convert git branch/tag names into SHA1
-    local sha1
-    sha1=$(git_rev_parse "$dir" "$ref" "$remote")
-    # Checkout
-    git -C "$dir" checkout --detach "$sha1"
+    git_checkout "$dir" "$ref" "$remote"
     )
 }