diff options
| author | herbelin | 2008-02-06 12:22:16 +0000 |
|---|---|---|
| committer | herbelin | 2008-02-06 12:22:16 +0000 |
| commit | 619a9aad46a82e9db859e9a7378c8f62e5e927a6 (patch) | |
| tree | 479721b97d60717fe376200940e067d746c36a81 | |
| parent | 316e114dd188f85ec657420989bf909ecfe9d006 (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-x | configure | 5 |
1 files changed, 5 insertions, 0 deletions
@@ -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 |
