diff --git a/scripts/fetch-develop.deps.sh b/scripts/fetch-develop.deps.sh index cc0f221a20..4fa1a4a22c 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=${curbranch#origin/} + echo "Determined branch to be $curbranch" # clone a specific branch of a github repo