path: root/vagrant
diff options
authoranonym <>2019-02-22 11:40:44 +0100
committeranonym <>2019-02-22 12:00:38 +0100
commitd910948ef2f141a7469f7675dec1e29c06ec3712 (patch)
tree1883c09fd3a304f7462109e97e77104fb9b23954 /vagrant
parent8bf53a97bde84fb7b871423fec887019548c3b58 (diff)
Build system: stop trying to be smart and fetch only the refs we need.
While the `git fetch origin "$(cat config/base_branch)"` approach works fine in my Vagrant setup, it fails on Jenkins for reasons not entirely clear to me. So let's just fetch everything, like before.
Diffstat (limited to 'vagrant')
1 files changed, 1 insertions, 4 deletions
diff --git a/vagrant/provision/assets/build-tails b/vagrant/provision/assets/build-tails
index 291a375..c6c5091 100755
--- a/vagrant/provision/assets/build-tails
+++ b/vagrant/provision/assets/build-tails
@@ -93,10 +93,7 @@ cd "${TAILS_GIT_DIR}"
git config remote.origin.fetch +refs/remotes/origin/*:refs/remotes/origin/*
# Ensure we have the same Git state as on the host
-git fetch origin "${GIT_REF}"
-if [ "${TAILS_MERGE_BASE_BRANCH}" = 1 ]; then
- git fetch origin "$(cat config/base_branch)"
+git fetch --tags
git checkout --force "${GIT_REF}"
git reset --hard "${GIT_COMMIT}"
git submodule update --init