From b0486e333d66603aae06942857c09a8cd18492d4 Mon Sep 17 00:00:00 2001 From: David Baker Date: Wed, 7 Jun 2017 10:35:08 +0100 Subject: [PATCH] Chop off 'origin/' when figuring out what branch we're on --- scripts/fetch-develop.deps.sh | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/scripts/fetch-develop.deps.sh b/scripts/fetch-develop.deps.sh index cc0f221a20..46a924ba78 100755 --- a/scripts/fetch-develop.deps.sh +++ b/scripts/fetch-develop.deps.sh @@ -25,6 +25,11 @@ else fi fi +# Chop 'origin' off the start as jenkins ends up using +# branches on the origin, but this doesn't work if we +# specify the branch when cloning. +curbranch=`echo "$curbranch" | sed -e 's/^origin\///'` + echo "Determined branch to be $curbranch" # clone a specific branch of a github repo