diff options
| -rw-r--r-- | Makefile.build | 4 | ||||
| -rw-r--r-- | Makefile.common | 17 |
2 files changed, 18 insertions, 3 deletions
diff --git a/Makefile.build b/Makefile.build index 0ab057a9d3..56ef6b1fdd 100644 --- a/Makefile.build +++ b/Makefile.build @@ -91,7 +91,7 @@ STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)" TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) COQOPTS=$(COQ_XML) $(NATIVECOMPUTE) -BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile +BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile # The SHOW and HIDE variables control whether make will echo complete commands # or only abbreviated versions. @@ -181,7 +181,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 0876700fa9..aacd801b52 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 |