diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2016-07-05 18:22:53 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-07-05 18:29:00 +0200 |
commit | b2dd4dd979577e4f384750872f7f0e7f9bd8df94 (patch) | |
tree | 613c86859810558ec7127a47fc6469ec207b7ca5 /Makefile.common | |
parent | 82ed3089485ebe0b722d8505ddbd89d73570b8f9 (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.common | 22 |
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 |