diff options
| author | courant | 2002-03-12 10:18:54 +0000 |
|---|---|---|
| committer | courant | 2002-03-12 10:18:54 +0000 |
| commit | 504114a41692bbc1e1621d84cadff4773f23bf35 (patch) | |
| tree | 3eb45b7b3711be9e8d332292578ae8e64ad82e0c /Makefile | |
| parent | 23e18510e55ae05312f59be1fc9598246b6507bb (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2525 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 17 |
1 files changed, 10 insertions, 7 deletions
@@ -59,7 +59,7 @@ CAMLP4DEPS=sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$$|\1|p' COQINCLUDES= # coqtop includes itself the needed paths GLOB= # is "-dump-glob file" when making the doc -BOOTCOQTOP=$(COQTOP) -boot -$(BEST) $(COQINCLUDES) $(GLOB) +BOOTCOQTOP=$(BESTCOQTOP) -boot -$(BEST) $(COQINCLUDES) $(GLOB) ########################################################################### # Objects files @@ -247,11 +247,12 @@ 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:: binaries states theories contrib tools +coqbinaries:: ${COQBINARIES} -binaries:: $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(BESTCOQTOP) $(COQTOP) \ - $(COQINTERFACE) +world: coqbinaries states theories contrib tools $(COQTOPOPT): $(COQMKTOP) $(CMX) $(USERTACCMX) $(COQMKTOP) -opt $(MLINCLUDES) -o $@ @@ -527,10 +528,10 @@ INTERFACEV0 = contrib/interface/Centaur.vo contrib/interface/vernacrc FOURIERVO = contrib/fourier/Fourier_util.vo contrib/fourier/Fourier.vo contrib/interface/Centaur.vo: contrib/interface/Centaur.v $(INTERFACE) - $(COQTOP) -boot -byte $(COQINCLUDES) -compile $* + $(BESTCOQTOP) -boot -byte $(COQINCLUDES) -compile $* contrib/interface/AddDad.vo: contrib/interface/AddDad.v $(INTERFACE) states/initial.coq - $(COQTOP) -boot -byte $(COQINCLUDES) -compile $* + $(BESTCOQTOP) -boot -byte $(COQINCLUDES) -compile $* CONTRIBVO = $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \ $(CORRECTNESSVO)\ @@ -897,10 +898,12 @@ depend: beforedepend $(MAKE) -f Makefile.dep $(ML4FILESML) # 3. We compute the dependencies inside the .ml files using ocamldep $(OCAMLDEP) $(DEPFLAGS) */*.mli */*/*.mli */*.ml */*/*.ml > .depend -# 4. We express dependencies of .cmo files w.r.t their grammars +# 4. We express dependencies of .cmo and .cmx files w.r.t their grammars for f in $(ML4FILES); do \ printf "%s" `dirname $$f`/`basename $$f .ml4`".cmo: " >> .depend; \ echo `$(CAMLP4DEPS) $$f` >> .depend; \ + printf "%s" `dirname $$f`/`basename $$f .ml4`".cmx: " >> .depend; \ + echo `$(CAMLP4DEPS) $$f` >> .depend; \ done # 5. Finally, we erase the generated .ml files rm -f $(ML4FILESML) |