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-basic-overlay.sh | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'dev/ci/ci-basic-overlay.sh')

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index b7faea13ed..5c882ee856 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -11,6 +11,8 @@
 ########################################################################
 : "${mathcomp_CI_BRANCH:=master}"
 : "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp.git}"
+: "${oddorder_CI_BRANCH:=master}"
+: "${oddorder_CI_GITURL:=https://github.com/math-comp/odd-order.git}"
 
 ########################################################################
 # UniMath
-- 
cgit v1.2.3