[travis] Make the git_checkout function more reliable.

This commit also documents the behavior of said function;
and fix the location of the ssreflect clone to an absolute
path (this is now necessary).

1 files changed, 15 insertions, 14 deletions

diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 94fd00c0d..6f624ab6e 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -8,28 +8,29 @@ export PATH=`pwd`/bin:$PATH
 
 ls `pwd`/bin
 
+# Where we clone and build external developments
+CI_BUILD_DIR=`pwd`/_build_ci
+
 # Maybe we should just use Ruby...
 mathcomp_CI_BRANCH=master
 mathcomp_CI_GITURL=https://github.com/math-comp/math-comp.git
+mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp
 
-# Where we clone and build external developments
-CI_BUILD_DIR=`pwd`/_build_ci
-
-# git_checkout branch
+# git_checkout branch url dest will create a git repository
+# in <dest> (if it does not exist already) and checkout the
+# remote branch <branch> from <url>
 git_checkout()
 {
   local _BRANCH=${1}
   local _URL=${2}
   local _DEST=${3}
 
-  mkdir -p ${CI_BUILD_DIR}
-  cd ${CI_BUILD_DIR}
-
-  if [ ! -d ${_DEST} ] ; then
-    echo "Checking out ${_DEST}"
-    git clone --depth 1 -b ${_BRANCH} ${_URL} ${_DEST}
-  fi
-  ( cd ${_DEST} && git pull &&
+  mkdir -p ${_DEST}
+  ( cd ${_DEST}                                                && \
+    if [ ! -d .git ] ; then git clone --depth 1 ${_URL} . ; fi && \
+    echo "Checking out ${_DEST}"                               && \
+    git fetch ${_URL} ${_BRANCH}                               && \
+    git checkout FETCH_HEAD                                    && \
     echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" )
 }
 
@@ -43,8 +44,8 @@ install_ssreflect()
 {
   echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r'
 
-  checkout_mathcomp math-comp
-  ( cd math-comp/mathcomp            && \
+  checkout_mathcomp ${mathcomp_CI_DIR}
+  ( cd ${mathcomp_CI_DIR}/mathcomp   && \
     sed -i.bak '/ssrtest/d'     Make && \
     sed -i.bak '/odd_order/d'   Make && \
     sed -i.bak '/all\/all.v/d'  Make && \