diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-24 01:06:46 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-24 01:11:28 +0200 |
| commit | c954bb5600e39f2cc19a96bcbb912ac694b3c16a (patch) | |
| tree | f233980fe76663f29748f604227900985e9d0779 /Makefile.install | |
| parent | 9165bd2489842af64dbe098ed5906fe69e687bfe (diff) | |
Makefile.install: fix the install of plugin cmi
Now that the plugins are packed, a plugin forms now a unique
compilation unit, and we only need to install the main cmi file of
this plugin (foo_plugin.cmi).
Btw, better variable names (e.g. OMEGACMO instead of OMEGACMA) and
some other cleanup in Makefile.common (no more INITPLUGINS variable,
for instance).
Diffstat (limited to 'Makefile.install')
| -rw-r--r-- | Makefile.install | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/Makefile.install b/Makefile.install index ed29bc1e7..09c3331f0 100644 --- a/Makefile.install +++ b/Makefile.install @@ -9,6 +9,11 @@ # This makefile regroups installation rules # It is included by Makefile.build +# NOTA: currently, the install rules below assume that everything needed +# has already been correctly built. In particular, this is *not* enforced +# by dependencies between rules, so do *not* try overly clever things like +# 'make world install' in one unique command + ifeq ($(LOCAL),true) install: @echo "Nothing to install in a local build!" @@ -16,6 +21,8 @@ else install: install-coq install-coqide install-doc-$(WITHDOC) endif +# NOTA: for install-coqide, see Makefile.ide + install-doc-all: install-doc install-doc-no: @@ -72,12 +79,15 @@ install-tools: $(INSTALLLIB) tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc $(INSTALLBIN) $(TOOLS) $(FULLBINDIR) -# The list of .cmi to install, including the ones obtained -# from .mli without .ml, and the ones obtained from .ml without .mli +# The list of .cmi to install, including in particular +# - the ones obtained from .mli without .ml +# - the ones of modules in core cma's +# - the ones corresponding to packed plugins INSTALLCMI = $(sort \ $(filter-out checker/% ide/% tools/%, $(MLIFILES:.mli=.cmi)) \ - $(foreach lib,$(CORECMA) $(PLUGINSCMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES))))) + $(foreach lib,$(CORECMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES))))) \ + $(PLUGINS:.cmo:.cmi) install-devfiles: $(MKDIR) $(FULLBINDIR) |