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

2 files changed, 18 insertions, 3 deletions

diff --git a/Makefile.build b/Makefile.build
index 0ab057a9d3..56ef6b1fdd 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -91,7 +91,7 @@ STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)"
 TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
 
 COQOPTS=$(COQ_XML) $(NATIVECOMPUTE)
-BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile
+BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile
 
 # The SHOW and HIDE variables control whether make will echo complete commands 
 # or only abbreviated versions. 
@@ -181,7 +181,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
diff --git a/Makefile.common b/Makefile.common
index 0876700fa9..aacd801b52 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -45,7 +45,22 @@ ifeq ($(HASNATDYNLINK)-$(BEST),false-opt)
  # static link of plugins, do not mention them in .v.d
  DYNDEP:=-dyndep no
 else
- DYNDEP:=-dyndep $(BEST)
+ DYNDEP:=-dyndep var
+endif
+
+# Which coqtop do we use to build .vo file ? The best ;-)
+# Note: $(BEST) could be overridden by the user if a byte build is desired
+# Note: coqdep -dyndep var will use $(DYNOBJ) and $(DYNLIB) extensions
+# for Declare ML Module files.
+
+ifeq ($(BEST),opt)
+COQTOPBEST:=$(COQTOPEXE)
+DYNOBJ:=.cmxs
+DYNLIB:=.cmxs
+else
+COQTOPBEST:=$(COQTOPBYTE)
+DYNOBJ:=.cmo
+DYNLIB:=.cma
 endif
 
 INSTALLBIN:=install