aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorherbelin2008-02-06 12:22:16 +0000
committerherbelin2008-02-06 12:22:16 +0000
commit619a9aad46a82e9db859e9a7378c8f62e5e927a6 (patch)
tree479721b97d60717fe376200940e067d746c36a81
parent316e114dd188f85ec657420989bf909ecfe9d006 (diff)
Protection contre l'erreur mentionnée dans le rapport de bug 1790
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10513 85f007b7-540e-0410-9357-904b9bb8a0f7
-rwxr-xr-xconfigure5
1 files changed, 5 insertions, 0 deletions
diff --git a/configure b/configure
index b00c259260..c532d3635e 100755
--- a/configure
+++ b/configure
@@ -401,6 +401,11 @@ esac
if [ "$camlp5dir" != "" ]; then
CAMLP4=$camlp5dir
CAMLP4LIB=$camlp5dir
+ if [ ! -f $camlp5dir/camlp5.cma ]; then
+ echo "Cannot find camlp5 libraries in $camlp5dir (camlp5.cma not found)"
+ echo "Configuration script failed!"
+ exit 1
+ fi
camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
elif [ "$CAMLTAG" = "OCAML310" ]; then
if [ -x "${CAMLLIB}/camlp5" ]; then