diff options
| author | Maxime Dénès | 2017-02-07 18:13:51 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-02-07 18:13:51 +0100 |
| commit | 93fb83feefbed738aae98b23715465d8b92816da (patch) | |
| tree | 5095610d4ace8f92bbcbc5f254b27f9d4f281f23 /dev | |
| parent | d8e918e48048b09f859421861ba0bf487e5a0d48 (diff) | |
| parent | fedf877e14ed75fd7156a97f5bd6dcdc9c6ffcef (diff) | |
Merge PR#425: [travis] [External CI] [geocoq] don't build slow file
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/ci/ci-geocoq.sh | 6 |
1 files changed, 5 insertions, 1 deletions
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} ) |