From ed91bf1fce168026675f986a0069ca596ad2b806 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 14 May 2018 22:29:38 +0200
Subject: [ci] Don't build lite versions of CI developments.

In the original Travis CI setup, the per-job time limit was an
issue. However, Gitlab has much improved this problem due to

 a) Coq not being built for each contrib,
 b) user-configurable time limit.

We thus disable the expensive builds from Travis:

 `fiat-crypto`, `formal-topology`, `geocoq`, `iris-lambda-rust`,
 `math-comp`, `unimath`, `vst`

and instruct Gitlab to build [`geocoq`, `math-comp`, `unimath`, `vst`]
in full.

We also update the `math-comp` script as the `odd-order` theorem lives
in a separate repository and it is a key CI case.
---
 dev/ci/ci-geocoq.sh | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'dev/ci/ci-geocoq.sh')

diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
index bd1d88993c..920272bcfb 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -7,6 +7,4 @@ GeoCoq_CI_DIR="${CI_BUILD_DIR}/GeoCoq"
 
 git_checkout "${GeoCoq_CI_BRANCH}" "${GeoCoq_CI_GITURL}" "${GeoCoq_CI_DIR}"
 
-( cd "${GeoCoq_CI_DIR}"                                     && \
-  ./configure-ci.sh                                       && \
-  make )
+( cd "${GeoCoq_CI_DIR}" && ./configure.sh && make )
-- 
cgit v1.2.3