diff options
| author |  notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-24 11:41:12 +0000 |
|---|---|---|
| committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-24 11:41:12 +0000 |
| commit | 4823449f7f3800835bfd5ebc4de5bdf407fdc2c2 (patch) | |
| tree | aea77208ed5b783f4f00c5c6679f1b1bdbbab264 /Makefile.build | |
| 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 'Makefile.build')
| -rw-r--r-- | Makefile.build | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.build b/Makefile.build index a87d0032b..e91ffb86a 100644 --- a/Makefile.build +++ b/Makefile.build @@ -563,7 +563,7 @@ states/initial.coq: states/MakeInitial.v $(INITVO) $(VO_TOOLS_STRICT) | states/M theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_STRICT) | theories/Init/%.v.d $(VO_TOOLS_ORDER_ONLY) $(SHOW)'COQC -nois $<' $(HIDE)rm -f theories/Init/$*.glob - $(HIDE)$(BOOTCOQTOP) -dump-glob theories/Init/$*.glob -nois -compile theories/Init/$* + $(HIDE)$(BOOTCOQTOP) -nois -compile theories/Init/$* theories/Numbers/Natural/BigN/NMake.v: theories/Numbers/Natural/BigN/NMake_gen.ml $(OCAML) $< > $@ @@ -875,7 +875,7 @@ endif %.vo %.glob: %.v states/initial.coq $(VO_TOOLS_STRICT) | %.v.d $(VO_TOOLS_ORDER_ONLY) $(SHOW)'COQC $<' $(HIDE)rm -f $*.glob - $(HIDE)$(BOOTCOQTOP) -dump-glob $*.glob -compile $* + $(HIDE)$(BOOTCOQTOP) -compile $* ifdef VALIDATE $(SHOW)'COQCHK $(shell basename $*)' $(HIDE)$(BESTCHICKEN) -silent -norec $(shell basename $*) \ |