Asks camlp5 binary in path its location

before looking in CAMLLIB/camlp5 folder

Patch by Thomas Braibant

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

1 files changed, 22 insertions, 16 deletions

diff --git a/configure b/configure
index 5f91aa1f6..1a6b72604 100755
--- a/configure
+++ b/configure
@@ -484,23 +484,29 @@ case $usecamlp5 in
     CAMLP4=camlp5
     CAMLP4MOD=gramlib
     if [ "$camlp5dir" != "" ]; then
-        if [ -f "$camlp5dir/${CAMLP4MOD}.cma" ]; then
-            CAMLP4LIB=$camlp5dir
-            FULLCAMLP4LIB=$camlp5dir
-        else
-            echo "Cannot find camlp5 libraries in $camlp5dir (camlp5.cma not found)."
-            echo "Configuration script failed!"
-            exit 1
-        fi
-    elif [ -f "${CAMLLIB}/camlp5/${CAMLP4MOD}.cma" ]; then
-        CAMLP4LIB=+camlp5
-        FULLCAMLP4LIB=${CAMLLIB}/camlp5
-    elif [ -f "${CAMLLIB}/site-lib/${CAMLP4MOD}.cma" ]; then
-        CAMLP4LIB=+site-lib/camlp5
-        FULLCAMLP4LIB=${CAMLLIB}/site-lib/camlp5
+	if [ -f "$camlp5dir/${CAMLP4MOD}.cma" ]; then
+	    CAMLP4LIB=$camlp5dir
+	    FULLCAMLP4LIB=$camlp5dir
+	else
+	    echo "Cannot find camlp5 libraries in $camlp5dir (camlp5.cma not found)."
+	    echo "Configuration script failed!"
+	    exit 1
+	fi
     else
-        echo "No Camlp5 installation found. Looking for Camlp4 instead..."
-        usecamlp5=no
+	camlp5dir="$(camlp5 -where)"
+	if [ "$camlp5dir" != "" ]; then
+	    CAMLP4LIB=$camlp5dir
+	    FULLCAMLP4LIB=$camlp5dir
+	elif [ -f "${CAMLLIB}/camlp5/${CAMLP4MOD}.cma" ]; then
+            CAMLP4LIB=+camlp5
+	    FULLCAMLP4LIB=${CAMLLIB}/camlp5
+	elif [ -f "${CAMLLIB}/site-lib/${CAMLP4MOD}.cma" ]; then
+            CAMLP4LIB=+site-lib/camlp5
+	    FULLCAMLP4LIB=${CAMLLIB}/site-lib/camlp5
+	else
+	    echo "No Camlp5 installation found. Looking for Camlp4 instead..."
+	    usecamlp5=no
+	fi
     fi
 esac