diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-06-14 19:00:23 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-14 19:00:23 +0200 |
commit | e1d68573015883301cb401861e10233f6442d9ec (patch) | |
tree | b62f4d6f0f2cfdd09cbe6080f66ec8c92024fbce /.travis.yml | |
parent | 54063fcda793ca8179047ff2a2c9863891a97acd (diff) | |
parent | 9a14a95f96c77ff3850d694637738358c164f4b5 (diff) |
Merge PR#749: Normalize deprecation notices of ./configure
Diffstat (limited to '.travis.yml')
-rw-r--r-- | .travis.yml | 2 |
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' |