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


From ba36aab9ad9a3d210211e1d4527dd0f6f493ca05 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 7 Mar 2017 16:14:39 +0100
Subject: [travis] Change headband for wider compatibility.

---
 dev/ci/ci-math-comp.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(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 2eb150cb52..1b6c6fb847 100755
--- a/dev/ci/ci-math-comp.sh
+++ b/dev/ci/ci-math-comp.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 # $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
-- 
cgit v1.2.3


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