aboutsummaryrefslogtreecommitdiffhomepage
path: root/.travis.yml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-06-14 19:00:23 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-06-14 19:00:23 +0200
commite1d68573015883301cb401861e10233f6442d9ec (patch)
treeb62f4d6f0f2cfdd09cbe6080f66ec8c92024fbce /.travis.yml
parent54063fcda793ca8179047ff2a2c9863891a97acd (diff)
parent9a14a95f96c77ff3850d694637738358c164f4b5 (diff)
Merge PR#749: Normalize deprecation notices of ./configure
Diffstat (limited to '.travis.yml')
-rw-r--r--.travis.yml2
1 files changed, 1 insertions, 1 deletions
diff --git a/.travis.yml b/.travis.yml
index 3d4350dca..01680583f 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -158,7 +158,7 @@ script:
- set -e
- echo 'Configuring Coq...' && echo -en 'travis_fold:start:coq.config\\r'
-- ./configure -local -usecamlp5 -native-compiler ${NATIVE_COMP} ${EXTRA_CONF}
+- ./configure -local -native-compiler ${NATIVE_COMP} ${EXTRA_CONF}
- echo -en 'travis_fold:end:coq.config\\r'
- echo 'Building Coq...' && echo -en 'travis_fold:start:coq.build\\r'