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