aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.common
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-07-05 18:22:53 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-07-05 18:29:00 +0200
commitb2dd4dd979577e4f384750872f7f0e7f9bd8df94 (patch)
tree613c86859810558ec7127a47fc6469ec207b7ca5 /Makefile.common
parent82ed3089485ebe0b722d8505ddbd89d73570b8f9 (diff)
Revert "Merge remote-tracking branch 'github/pr/229' into trunk"
This reverts commit b2f8f9edd5c1bb0a9c8c4f4b049381b979d3e385, reversing changes made to da99355b4d6de31aec5a660f7afe100190a8e683. Hugo asked for more discussion on this topic, and it was not in the roadmap. I merged it prematurely because I thought there was a consensus. Also, I missed that it was changing coq_makefile. Sorry about that.
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common22
1 files changed, 3 insertions, 19 deletions
diff --git a/Makefile.common b/Makefile.common
index aacd801b5..49fe1fd93 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -41,26 +41,10 @@ CSDPCERT:=plugins/micromega/csdpcert$(EXE)
# Object and Source files
###########################################################################
-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
+ifeq ($(HASNATDYNLINK)-$(BEST),true-opt)
+ DEPNATDYN:=
else
-COQTOPBEST:=$(COQTOPBYTE)
-DYNOBJ:=.cmo
-DYNLIB:=.cma
+ DEPNATDYN:=-natdynlink no
endif
INSTALLBIN:=install