diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-24 19:59:08 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-24 19:59:08 +0000 |
| commit | 0832467f0b4445f7b4c5f8e9ab417e585362ed9c (patch) | |
| tree | 6dfac62c782faf282c192509be02fc443d120218 /dev/ocamldebug-v7.template | |
| parent | 41e0e7066c16078bc798d16a6d8d2eb66d10b59c (diff) | |
Paramètrage de ocamldebug-v7 par configure à partir d'un 'template'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@949 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/ocamldebug-v7.template')
| -rw-r--r-- | dev/ocamldebug-v7.template | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/dev/ocamldebug-v7.template b/dev/ocamldebug-v7.template new file mode 100644 index 000000000..362f63b9e --- /dev/null +++ b/dev/ocamldebug-v7.template @@ -0,0 +1,34 @@ +#!/bin/sh + +# wrap around ocamldebug for Coq + +export COQTOP=COQTOPDIRECTORY +export COQLIB=COQLIBDIRECTORY +export COQTH=$COQLIB/theories +export CAMLP4LIB=CAMLP4LIBDIRECTORY +CAMLBIN=CAMLBINDIRECTORY +OCAMLDEBUG=$CAMLBIN/ocamldebug + +args="" +coqdebug="no" +for op in $* + do case `basename $op` in + coq-debug-programs.out) + coqdebug="yes" + args="-is programs.coq";; + coq*) coqdebug="yes";; + esac +done + +case $coqdebug in + yes) + exec $OCAMLDEBUG \ + -I $CAMLP4LIB \ + -I $COQTOP/lib -I $COQTOP/kernel \ + -I $COQTOP/library -I $COQTOP/pretyping -I $COQTOP/parsing \ + -I $COQTOP/proofs -I $COQTOP/tactics \ + -I $COQTOP/toplevel -I $COQTOP/dev \ + -I $COQTOP/contrib/omega -I $COQTOP/contrib/ring \ + $* $args;; + *) exec $OCAMLDEBUG $*;; +esac |