aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--Makefile.build4
-rw-r--r--Makefile.common17
2 files changed, 18 insertions, 3 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
diff --git a/Makefile.common b/Makefile.common
index 3d4e7829a..d19cbd6ad 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