From 710c1e1f49ce834acb9488704bcbbf13c4ebaf91 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 7 Mar 2017 23:30:29 +0100
Subject: [travis] Adding a template file and using it for all targets.

---
 dev/ci/ci-math-comp.sh | 6 ++++--
 1 file changed, 4 insertions(+), 2 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 1b6c6fb847..bb8188da4e 100755
--- a/dev/ci/ci-math-comp.sh
+++ b/dev/ci/ci-math-comp.sh
@@ -4,10 +4,12 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-checkout_mathcomp math-comp
+mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp
+
+checkout_mathcomp ${mathcomp_CI_DIR}
 
 # odd_order takes too much time for travis.
-( cd math-comp/mathcomp                           && \
+( cd ${mathcomp_CI_DIR}/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