diff options
author | 2002-03-05 15:51:11 +0000 | |
---|---|---|
committer | 2002-03-05 15:51:11 +0000 | |
commit | c877c64b4592d77c28c7932f73d4bb98142116b2 (patch) | |
tree | 8b9fffdeb2d41b9e484662cfa83024cd8359ea36 /Makefile | |
parent | 9e5122c6fa0d6907a8c7a1464831087fb0cfb421 (diff) |
ajout d'une entree 'binaries' pour recompiler coq mais pas les theories
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2515 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 13 |
1 files changed, 7 insertions, 6 deletions
@@ -247,10 +247,11 @@ BESTCOQTOP=bin/coqtop.$(BEST)$(EXE) COQTOP=bin/coqtop$(EXE) COQINTERFACE=bin/coq-interface$(EXE) bin/parser$(EXE) -COQBINARIES= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(BESTCOQTOP) $(COQTOP) \ - $(COQINTERFACE) -world: $(COQBINARIES) states theories contrib tools +world:: binaries states theories contrib tools + +binaries:: $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(BESTCOQTOP) $(COQTOP) \ + $(COQINTERFACE) $(COQTOPOPT): $(COQMKTOP) $(CMX) $(USERTACCMX) $(COQMKTOP) -opt $(MLINCLUDES) -o $@ @@ -326,14 +327,14 @@ clean:: # tests ########################################################################### -check: $(BESTCOQTOP) +check:: $(BESTCOQTOP) cd test-suite; ./check -$(BEST) ########################################################################### # theories and states ########################################################################### -states: states/barestate.coq states/initial.coq +states:: states/barestate.coq states/initial.coq SYNTAXPP=syntax/PPConstr.v syntax/PPCases.v syntax/PPTactic.v @@ -566,7 +567,7 @@ COQTEX=bin/coq-tex$(EXE) COQVO2XML=bin/coq_vo2xml$(EXE) RUNCOQVO2XML=coq_vo2xml$(EXE) # Uses the one in PATH and not the one in bin -tools: $(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQVO2XML) dev/top_printers.cmo +tools:: $(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQVO2XML) dev/top_printers.cmo COQDEPCMO=config/coq_config.cmo tools/coqdep_lexer.cmo tools/coqdep.cmo |