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 /plugins/syntax/string_syntax_plugin.mlpack | |
| 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 'plugins/syntax/string_syntax_plugin.mlpack')
0 files changed, 0 insertions, 0 deletions