diff options
| author | notin | 2008-06-24 11:41:12 +0000 |
|---|---|---|
| committer | notin | 2008-06-24 11:41:12 +0000 |
| commit | 4823449f7f3800835bfd5ebc4de5bdf407fdc2c2 (patch) | |
| tree | aea77208ed5b783f4f00c5c6679f1b1bdbbab264 /tools/coq_makefile.ml4 | |
| parent | de45178c0b684a211fa61866e82b045f12f85ffe (diff) | |
Suppression de l'option -dump-glob et ajout d'une option -no-glob
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11167 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coq_makefile.ml4')
| -rw-r--r-- | tools/coq_makefile.ml4 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index 3138ce4eff..2dfac4e187 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -136,15 +136,15 @@ let implicit () = print "%.ml.d: %.ml\n"; print "\t$(CAMLBIN)ocamldep -slash $(ZFLAGS) $(PP) \"$<\" > \"$@\"\n\n" and v_rule () = - print "%.vo %.glob: %.v\n\t$(COQC) -dump-glob $*.glob $(COQDEBUG) $(COQFLAGS) $*\n\n"; + print "%.vo %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; print "%.vi: %.v\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n"; print "%.g: %.v\n\t$(GALLINA) $<\n\n"; print "%.tex: %.v\n\t$(COQDOC) -latex $< -o $@\n\n"; - print "%.html: %.v %.glob\n\t$(COQDOC) -glob-from $*.glob -html $< -o $@\n\n"; + print "%.html: %.v %.glob\n\t$(COQDOC) -html $< -o $@\n\n"; print "%.g.tex: %.v\n\t$(COQDOC) -latex -g $< -o $@\n\n"; - print "%.g.html: %.v %.glob\n\t$(COQDOC) -glob-from $*.glob -html -g $< -o $@\n\n"; + print "%.g.html: %.v %.glob\n\t$(COQDOC) -html -g $< -o $@\n\n"; print "%.v.d: %.v\n"; - print "\t$(COQDEP) -glob -slash $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" + print "\t$(COQDEP) -slash $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in if !some_mlfile then ml_rules (); if !some_vfile then v_rule () |