From 30a2def37ecdeeed24325089a0b0ca264100389c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 7 Feb 2017 19:37:15 +0100
Subject: [travis] [External CI] Factor out math-comp installs.

We make math-comp overlays easier, we also start structuring the
scripts a bit more.
---
 dev/ci/ci-math-comp.sh | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'dev/ci/ci-math-comp.sh')

diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh
index b833792419..2eb150cb52 100755
--- a/dev/ci/ci-math-comp.sh
+++ b/dev/ci/ci-math-comp.sh
@@ -4,10 +4,10 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-git clone --depth 3 https://github.com/math-comp/math-comp.git
+checkout_mathcomp math-comp
 
 # odd_order takes too much time for travis.
-( cd math-comp/mathcomp                              && \
-     sed -i.bak '/PFsection/d'                  Make && \
-     sed -i.bak '/stripped_odd_order_theorem/d' Make && \
-     make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all )
+( cd math-comp/mathcomp                           && \
+  sed -i.bak '/PFsection/d'                  Make && \
+  sed -i.bak '/stripped_odd_order_theorem/d' Make && \
+  make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all )
-- 
cgit v1.2.3