- Correction d'un bug de coq_makefile sur les variables CAMLLIBS et

  COQLIBS.
- Ajout d'un message d'erreur si Camlp5 est compilé en mode strict




git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10746 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 0 deletions

diff --git a/configure b/configure
index 814e92a552..4ae429f90d 100755
--- a/configure
+++ b/configure
@@ -412,6 +412,11 @@ if [ "$camlp5dir" != "" ]; then
 	exit 1
     fi
     camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
+    if [ `$camlp4oexec -pmode 2>&1` = "strict" ]; then 
+	echo "Error: Camlp5 found, but in strict mode!"
+	echo "Please compile Camlp5 in transitional mode."
+	exit 1
+    fi
 elif [ "$CAMLTAG" = "OCAML310" ]; then
     if [ -x "${CAMLLIB}/camlp5" ]; then 
         CAMLP4LIB=+camlp5
@@ -424,6 +429,11 @@ elif [ "$CAMLTAG" = "OCAML310" ]; then
     fi
     CAMLP4=camlp5
     camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
+    if [ `$camlp4oexec -pmode 2>&1` = "strict" ]; then 
+	echo "Error: Camlp5 found, but in strict mode!"
+	echo "Please compile Camlp5 in transitional mode."
+	exit 1
+    fi
 else 
     CAMLP4=camlp4
     CAMLP4LIB=+camlp4