diff options
| author | Enrico Tassi | 2017-08-09 14:43:48 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2017-08-29 14:25:51 +0200 |
| commit | 534b8afafc763b382fb3fa747bb95a9a57676d4c (patch) | |
| tree | 63d82a6709b0dbe3e8b96d841b482ae59f88305c /tools | |
| parent | 10a3ad4074fbc85ca146d44449c1fe433515e3db (diff) | |
coq_makefile: build/use .cma for packed plugins
The build chain is always
ml -> cmo -> cma
ml -> cmx -> cmxa -> cmxs
If we are packing, then it becomes
ml -> cmo \
ml -> cmo --> cmo -> cma
ml -> cmo /
ml -> cmxo \
ml -> cmxo --> cmxo -> cmxa -> cmxs
ml -> cmxo /
The interest of always having a .cma or .cmxa is that such file can
carry linking flags, that in findlib terms means which
-package was use to build the plugin.
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 9f891afe53..f6fe6ddeb1 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -151,7 +151,7 @@ OPT?= # The DYNOBJ and DYNLIB variables are used by "coqdep -dyndep var" in .v.d ifeq '$(OPT)' '-byte' USEBYTE:=true -DYNOBJ:=.cmo +DYNOBJ:=.cma DYNLIB:=.cma else USEBYTE:= |