diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-29 15:13:13 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-30 17:48:04 +0200 |
| commit | 9b175072b04195d612615c68ff379dd09aa06f0f (patch) | |
| tree | c4581781f466ad0d026b0f2b66730d2dcc2a8c14 /Makefile.common | |
| parent | 419e7cac23d7b8ac97d46a6c0d3228d591273d2b (diff) | |
Makefile: $(BEST) controls which coqtop is used to build .vo
This allows to grant a wish by Hugo: to build coqtop.byte and prelude
with it, you could do:
make -j BEST=byte states
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 17 |
1 files changed, 16 insertions, 1 deletions
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 |