Merge PR#501: [travis] Fix iris-coq build.

1 files changed, 6 insertions, 2 deletions

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'`" )
 }