From 9a14a95f96c77ff3850d694637738358c164f4b5 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
Date: Thu, 8 Jun 2017 11:17:22 +0200
Subject: Normalize deprecation notices of ./configure

Always output a warning on stderr when a deprecated option is used.
---
 .travis.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to '.travis.yml')

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'
-- 
cgit v1.2.3