diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-06-08 11:17:22 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-06-11 10:26:07 +0200 |
| commit | 9a14a95f96c77ff3850d694637738358c164f4b5 (patch) | |
| tree | 8d1ba78033d0e209fbaba7ba7ace7980a67b0c41 /.travis.yml | |
| parent | 102d7418e399de646b069924277e4baea1badaca (diff) | |
Normalize deprecation notices of ./configure
Always output a warning on stderr when a deprecated option is used.
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 e79498124..13bdd6fb2 100644 --- a/.travis.yml +++ b/.travis.yml @@ -155,7 +155,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' |