diff options
authorNeels Hofmeyr <nhofmeyr@sysmocom.de>2017-06-23 04:13:30 +0200
committerNeels Hofmeyr <nhofmeyr@sysmocom.de>2017-06-23 04:13:30 +0200
commitb398b52ad5d69aeef0aba014264800bd041508c7 (patch)
parent2581b50408418c698b35e946633f129f1e7d238d (diff)
jenkins: fix: recent change broke jenkins build
Recent commit 851802b927ccfcb061a2774fdc5de12141426b5c introduces a build branch, which works fine, but only on the first run. A second run in the same repos can't delete the branch git is currently on. I've had enough of git being impossibly difficult in UI to simply checkout a hash or a branch now. Completely wipe out the git repository and clone a fresh one every time. Unfortunately, 'git clone -b' doesn't allow passing a commit hash, so we still need to do a clone-then-checkout dance. At least now we know it will work the same on every run. Change-Id: I6aca4c53a796312248a189b815dfc1198a173ed9
1 files changed, 5 insertions, 6 deletions
diff --git a/contrib/jenkins-build-common.sh b/contrib/jenkins-build-common.sh
index 779f965..895cd63 100644
--- a/contrib/jenkins-build-common.sh
+++ b/contrib/jenkins-build-common.sh
@@ -73,18 +73,17 @@ have_repo() {
cd "$base"
- if [ ! -d "$repo" ]; then
- git clone "$git_url/$repo" "$repo"
- fi
+ rm -rf "$repo"
+ git clone "$git_url/$repo" "$repo"
cd "$repo"
- git fetch origin
- # Figure out whether we need to prepend origin/ to find branches in upstream
+ # Figure out whether we need to prepend origin/ to find branches in upstream.
+ # Doing this allows using git hashes instead of a branch name.
if git rev-parse "origin/$branch"; then
- git branch -D build_branch || true
git checkout -b build_branch "$branch"
rm -rf *
git reset --hard "$branch"