summaryrefslogtreecommitdiff
path: root/ci
diff options
context:
space:
mode:
authorLi Haoyi <haoyi.sg@gmail.com>2018-02-04 04:34:51 -0800
committerLi Haoyi <haoyi.sg@gmail.com>2018-02-04 04:34:51 -0800
commit2b88c8275cfb0a5917103efdcde1166077f96649 (patch)
tree1aefeec4caa031efa15c3551c1e60f7e8112b77a /ci
parentf27c385385fbd14370b3112af64d64470068631c (diff)
downloadmill-2b88c8275cfb0a5917103efdcde1166077f96649.tar.gz
mill-2b88c8275cfb0a5917103efdcde1166077f96649.tar.bz2
mill-2b88c8275cfb0a5917103efdcde1166077f96649.zip
try to fix git head in test4.sh
Diffstat (limited to 'ci')
-rwxr-xr-xci/test4.sh3
1 files changed, 3 insertions, 0 deletions
diff --git a/ci/test4.sh b/ci/test4.sh
index 137cec0e..3ce6c1c1 100755
--- a/ci/test4.sh
+++ b/ci/test4.sh
@@ -2,6 +2,9 @@
set -eux
+# Force travis to create a git HEAD otherwise common operations don't work
+git checkout -B current
+
# Starting from scratch...
git clean -xdf