aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.common
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common22
1 files changed, 19 insertions, 3 deletions
diff --git a/Makefile.common b/Makefile.common
index 62bbbc4fd..b2e1d47df 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -41,10 +41,26 @@ CSDPCERT:=plugins/micromega/csdpcert$(EXE)
# Object and Source files
###########################################################################
-ifeq ($(HASNATDYNLINK)-$(BEST),true-opt)
- DEPNATDYN:=
+ifeq ($(HASNATDYNLINK)-$(BEST),false-opt)
+ # static link of plugins, do not mention them in .v.d
+ DYNDEP:=-dyndep no
+else
+ 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
- DEPNATDYN:=-natdynlink no
+COQTOPBEST:=$(COQTOPBYTE)
+DYNOBJ:=.cmo
+DYNLIB:=.cma
endif
INSTALLBIN:=install