aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-03-18 00:11:25 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-03-18 00:11:25 +0000
commitdafb5f443611cf0bfb4626f47d20d65149bd3fe0 (patch)
treedb6c2c7edf63ca299bb22cd72fc96de700e2e19f /dev
parent8bff8bbd620e54022c2fea81542bf1cbc18fafb0 (diff)
bug discharge (work_alist contenanti plein de fois les memes choses)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@323 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
-rwxr-xr-xdev/ocamldebug-v72
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/ocamldebug-v7 b/dev/ocamldebug-v7
index 5e9b2aa02..38572b720 100755
--- a/dev/ocamldebug-v7
+++ b/dev/ocamldebug-v7
@@ -3,7 +3,7 @@
# wrap around ocamldebug for Coq
# export COQTOP=`coqtop -where`
-export COQTOP=/home/jc/coq/V7
+export COQTOP=$HOME/coq/V7
export COQLIB=$COQTOP
export COQTH=$COQLIB/theories
export CAMLP4LIB=`camlp4 -where`