aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
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 \