summaryrefslogtreecommitdiff
path: root/configure
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2011-04-19 16:44:20 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2011-04-19 16:44:20 +0200
commit9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 (patch)
treea418d1edb3d53cdb4185b9719b7a70822cf5a24d /configure
parent6b691bbd2101fd39395c0d2135fd7c06a8915e14 (diff)
Imported Upstream version 8.3.pl2upstream/8.3.pl2
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure18
1 files changed, 4 insertions, 14 deletions
diff --git a/configure b/configure
index 9113f1e0..7cff4b97 100755
--- a/configure
+++ b/configure
@@ -6,7 +6,7 @@
#
##################################
-VERSION=8.3pl1
+VERSION=8.3pl2
VOMAGIC=08300
STATEMAGIC=58300
DATE=`LANG=C date +"%B %Y"`
@@ -411,12 +411,12 @@ esac
CAMLVERSION=`"$bytecamlc" -version`
case $CAMLVERSION in
- 1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.06|3.07*|3.08*|3.09.[012])
+ 1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.06|3.07*|3.08*|3.09*)
echo "Your version of Objective-Caml is $CAMLVERSION."
if [ "$force_caml_version" = "yes" ]; then
echo "*Warning* You are compiling Coq with an outdated version of Objective-Caml."
else
- echo " You need Objective-Caml 3.09.3 or later."
+ echo " You need Objective-Caml 3.10.2 or later."
echo " Configuration script failed!"
exit 1
fi;;
@@ -491,11 +491,6 @@ 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
else
case $CAMLTAG in
OCAML31*)
@@ -510,11 +505,6 @@ else
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
;;
*)
CAMLP4=camlp4
@@ -1094,4 +1084,4 @@ echo
echo "*Warning* To compile the system for a new architecture"
echo " don't forget to do a 'make archclean' before './configure'."
-# $Id: configure 13740 2010-12-23 12:37:18Z notin $
+# $Id: configure 14025 2011-04-19 07:19:00Z notin $