Permalink
Browse files

configure: camlp4 is now tried when camlp5 isn't found

 * When both camlp4 and camlp5 are installed, camlp5 is used by default,
   except when -usecamlp4 flag is given to ./configure.

 * Otherwise, ./configure pick automatically the available camlpX

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15349 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
letouzey
letouzey committed May 23, 2012
1 parent d05961c commit 756bafb378b087e18815812d1a01cdd031990804
Showing with 20 additions and 10 deletions.
  1. +20 −10 configure
View
@@ -537,7 +537,8 @@ esac
# (this should become configurable some day)
CAMLP4BIN=${CAMLBIN}
-if [ "$usecamlp5" = "yes" ]; then
+case $usecamlp5 in
+ yes)
CAMLP4=camlp5
CAMLP4MOD=gramlib
if [ "$camlp5dir" != "" ]; then
@@ -556,38 +557,47 @@ if [ "$usecamlp5" = "yes" ]; then
CAMLP4LIB=+site-lib/camlp5
FULLCAMLP4LIB=${CAMLLIB}/site-lib/camlp5
else
- echo "Objective Caml $CAMLVERSION found but no Camlp5 installed."
- echo "Configuration script failed!"
- exit 1
+ echo "No Camlp5 installation found. Looking for Camlp4 instead..."
+ usecamlp5=no
fi
+esac
+
+# If we're (still...) going to use Camlp5, let's check its version
- camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
- case `$camlp4oexec -v 2>&1` in
+case $usecamlp5 in
+ yes)
+ camlp4oexec=`echo "$camlp4oexec" | tr 4 5`
+ case `"$camlp4oexec" -v 2>&1` in
*4.0*|*5.00*)
echo "Camlp5 version < 5.01 not supported."
echo "Configuration script failed!"
exit 1;;
esac
+esac
+
+# We might now try to use Camlp4, either by explicit choice or
+# by lack of proper Camlp5 installation
-else # let's use camlp4
+case $usecamlp5 in
+ no)
CAMLP4=camlp4
CAMLP4MOD=camlp4lib
CAMLP4LIB=+camlp4
FULLCAMLP4LIB=${CAMLLIB}/camlp4
if [ ! -f "${FULLCAMLP4LIB}/${CAMLP4MOD}.cma" ]; then
- echo "Objective Caml $CAMLVERSION found but no Camlp4 installed."
+ echo "No Camlp4 installation found."
echo "Configuration script failed!"
exit 1
fi
camlp4oexec=${camlp4oexec}rf
- if [ "`$camlp4oexec 2>&1`" != "" ]; then
+ if [ "`"$camlp4oexec" 2>&1`" != "" ]; then
echo "Error: $camlp4oexec not found or not executable."
echo "Configuration script failed!"
exit 1
fi
-fi
+esac
# do we have a native compiler: test of ocamlopt and its version

0 comments on commit 756bafb

Please sign in to comment.