aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/Makefile.devel
diff options
context:
space:
mode:
authorGravatar coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-09-20 10:53:18 +0000
committerGravatar coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-09-20 10:53:18 +0000
commitdc16cbc0693d98c324c846e162d087d95d60f70d (patch)
treedd0d0ab7e38f8d8334827a3711fd62acbd1cd18c /dev/Makefile.devel
parenta406d5f7602f44daf8066faf399acbad3ba124fc (diff)
La notation with dependante + affichage dependante de moduels corrige
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3025 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/Makefile.devel')
-rw-r--r--dev/Makefile.devel2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/Makefile.devel b/dev/Makefile.devel
index 78318d59b..729e6147e 100644
--- a/dev/Makefile.devel
+++ b/dev/Makefile.devel
@@ -43,4 +43,4 @@ total:
#runs coqtop storing using the history file
run: $(TOPDIR)/coqtop
- ledit -h $(TOPDIR)/dev/debug_history -x $(TOPDIR)/coqtop
+ ledit -h $(TOPDIR)/dev/debug_history -x $(TOPDIR)/coqtop $(ARG) $(ARGS)