From 44b2c7979e1ea3a834f4e9bd2fcd631d568b895e Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 22 Mar 2017 17:17:33 +0100
Subject: [travis] Fix iris-coq build.

We need to do a bit of hacking, but it should be fine for the short
term.

c.f. https://gitlab.mpi-sws.org/FP/iris-coq/issues/83
---
 dev/ci/ci-common.sh | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'dev/ci/ci-common.sh')

diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index c94f150263..2711b7ecaa 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -25,12 +25,16 @@ git_checkout()
   local _URL=${2}
   local _DEST=${3}
 
+  # Allow an optional 4th argument for the commit
+  local _COMMIT=${4:-FETCH_HEAD}
+  local _DEPTH=$(if [ -z "${4}" ]; then echo "--depth 1"; fi)
+
   mkdir -p ${_DEST}
   ( cd ${_DEST}                                                && \
-    if [ ! -d .git ] ; then git clone --depth 1 ${_URL} . ; fi && \
+    if [ ! -d .git ] ; then git clone ${_DEPTH} ${_URL} . ; fi && \
     echo "Checking out ${_DEST}"                               && \
     git fetch ${_URL} ${_BRANCH}                               && \
-    git checkout FETCH_HEAD                                    && \
+    git checkout ${_COMMIT}                                    && \
     echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" )
 }
 
-- 
cgit v1.2.3