aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorherbelin2008-01-04 11:04:03 +0000
committerherbelin2008-01-04 11:04:03 +0000
commit8f3627741f9d4624851abc7de1f3bda28b7acf9a (patch)
treed3907e808c2e04be257ab3bfb398cdd7d900056a /dev
parent144e75ce2835e44542f5d90d751f06243e45ecc4 (diff)
Prise en compte de CAMLP4LIB via fichier configure plutôt que dynamiquement
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10418 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
-rw-r--r--dev/ocamldebug-coq.template6
1 files changed, 1 insertions, 5 deletions
diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template
index f921fb8a6c..978623ad22 100644
--- a/dev/ocamldebug-coq.template
+++ b/dev/ocamldebug-coq.template
@@ -6,12 +6,8 @@ export COQTOP=COQTOPDIRECTORY
export COQLIB=COQLIBDIRECTORY
export COQTH=$COQLIB/theories
CAMLBIN=CAMLBINDIRECTORY
+CAMLP4LIB=CAMLP4LIBDIRECTORY
OCAMLDEBUG=$CAMLBIN/ocamldebug
-if [ -x "$CAMLBIN/camlp5" ]; then
- export CAMLP4LIB=`$CAMLBIN/camlp5 -where`
-else
- export CAMLP4LIB=`$CAMLBIN/camlp4 -where`
-fi
exec $OCAMLDEBUG \
-I $CAMLP4LIB \