diff options
author | 2011-09-06 17:20:14 +0000 | |
---|---|---|
committer | 2011-09-06 17:20:14 +0000 | |
commit | 8421370e3b467799805b0b1289630228859aca1a (patch) | |
tree | 9aba534aa872231b34962f22eb98ba860f8b5d4d | |
parent | 524797ef22827cd634b1bb6d566f285cc5facc0f (diff) |
make world now builds fake_ide (to please coq-bench)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14462 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | Makefile.build | 6 | ||||
-rw-r--r-- | Makefile.common | 1 |
2 files changed, 4 insertions, 3 deletions
diff --git a/Makefile.build b/Makefile.build index 46512e28a..925e537f5 100644 --- a/Makefile.build +++ b/Makefile.build @@ -187,7 +187,7 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h # Main targets (coqmktop, coqtop.opt, coqtop.byte) ########################################################################### -coqbinaries:: ${COQBINARIES} ${CSDPCERT} +coqbinaries:: ${COQBINARIES} ${CSDPCERT} ${FAKEIDE} coq: coqlib tools coqbinaries @@ -379,7 +379,7 @@ MAKE_TSOPTS=-C test-suite -s BEST=$(BEST) VERBOSE=$(VERBOSE) check:: validate test-suite -test-suite: world $(ALLSTDLIB).v bin/fake_ide +test-suite: world $(ALLSTDLIB).v $(MAKE) $(MAKE_TSOPTS) clean $(MAKE) $(MAKE_TSOPTS) all $(HIDE)if grep -F 'Error!' test-suite/summary.log ; then false; fi @@ -511,7 +511,7 @@ $(COQDOC): $(COQDOCCMO:.cmo=$(BESTOBJ)) # fake_ide : for debugging or test-suite purpose, a fake ide simulating # a connection to coqtop -ideslave -bin/fake_ide: toplevel/ide_intf.mli toplevel/ide_intf.ml tools/fake_ide.ml +$(FAKEIDE): toplevel/ide_intf.mli toplevel/ide_intf.ml tools/fake_ide.ml $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,unix) diff --git a/Makefile.common b/Makefile.common index c27dd84ac..cd8f2063b 100644 --- a/Makefile.common +++ b/Makefile.common @@ -28,6 +28,7 @@ CHICKENBYTE:=bin/coqchk.byte$(EXE) CHICKENOPT:=bin/coqchk.opt$(EXE) BESTCHICKEN:=bin/coqchk.$(BEST)$(EXE) CHICKEN:=bin/coqchk$(EXE) +FAKEIDE:=bin/fake_ide$(EXE) ifeq ($(CAMLP4),camlp4) CAMLP4MOD:=camlp4lib |