From fedf877e14ed75fd7156a97f5bd6dcdc9c6ffcef Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 7 Feb 2017 15:58:02 +0100
Subject: [travis] [External CI] [geocoq] don't build slow file

Unfortunately `Ch16_coordinates_with_functions.v` takes alone ~15
minutes which is too much for Travis. Pity, because it was a nice use case.
---
 dev/ci/ci-geocoq.sh | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'dev/ci')

diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
index 7b5811dc4a..589a826e02 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -9,4 +9,8 @@ GeoCoq_CI_GITURL=https://github.com/GeoCoq/GeoCoq.git
 
 git clone --depth 1 -b ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL}
 
-( cd GeoCoq && ./configure.sh && make -j ${NJOBS} )
+( cd GeoCoq                                               && \
+  ./configure.sh                                          && \
+  sed -i.bak '/Ch16_coordinates_with_functions\.v/d' Make && \
+  coq_makefile -f Make -o Makefile                        && \
+  make -j ${NJOBS} )
-- 
cgit v1.2.3