From 073178a9821d10b72fe581d3ba7814afd7dfbb05 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
Date: Wed, 29 Jun 2016 15:13:13 +0200
Subject: 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
---
 Makefile.common | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index 0876700fa..aacd801b5 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
-- 
cgit v1.2.3