diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-29 15:13:13 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-30 17:48:04 +0200 |
| commit | 9b175072b04195d612615c68ff379dd09aa06f0f (patch) | |
| tree | c4581781f466ad0d026b0f2b66730d2dcc2a8c14 /Makefile.build | |
| parent | 419e7cac23d7b8ac97d46a6c0d3228d591273d2b (diff) | |
Makefile: $(BEST) controls which coqtop is used to build .vo
This allows to grant a wish by Hugo: to build coqtop.byte and prelude
with it, you could do:
make -j BEST=byte states
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 e3a74aaee..6203dd759 100644 --- a/Makefile.build +++ b/Makefile.build @@ -108,7 +108,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) # TIME="%C (%U user, %S sys, %e total, %M maxres)" COQOPTS=$(COQ_XML) $(NATIVECOMPUTE) -BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile +BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) ) MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) @@ -190,7 +190,7 @@ ifndef ORDER_ONLY_SEP $(error This Makefile needs GNU Make 3.81 or later (that is a version that supports the order-only dependency feature without major bugs.)) endif -VO_TOOLS_DEP := $(COQTOPEXE) +VO_TOOLS_DEP := $(COQTOPBEST) ifdef COQ_XML VO_TOOLS_DEP += $(COQDOC) endif |