From c954bb5600e39f2cc19a96bcbb912ac694b3c16a Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Fri, 24 Jun 2016 01:06:46 +0200 Subject: 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). --- Makefile.install | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) (limited to 'Makefile.install') 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) -- cgit v1.2.3