diff options
| author | letouzey | 2011-12-08 17:34:44 +0000 |
|---|---|---|
| committer | letouzey | 2011-12-08 17:34:44 +0000 |
| commit | 61c090d3e5779996c32a9314abe08592df434c30 (patch) | |
| tree | ef0116d0d12d1c9e8863d47d5dafc007b4b2c49f /Makefile.build | |
| parent | 8b3e22ced65c9393b19a2d6b3184d72ae8c32981 (diff) | |
Makefile: force the installation of all .cmi (and remove some obsolete .mli)
The previous code wasn't detecting and installing .cmi coming from
.mli without corresponding .ml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14783 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/Makefile.build b/Makefile.build index a21bee1b36..0e49c13819 100644 --- a/Makefile.build +++ b/Makefile.build @@ -621,6 +621,14 @@ 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 + +INSTALLCMI = $(sort \ + $(CONFIG:.cmo=.cmi) \ + $(filter-out checker/% ide/% tools/%, $(MLIFILES:.mli=.cmi)) \ + $(foreach lib,$(CORECMA) $(PLUGINSCMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES))))) + install-library: $(MKDIR) $(FULLCOQLIB) $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS) $(PLUGINSOPT) @@ -629,9 +637,7 @@ install-library: $(MKDIR) $(FULLCOQLIB)/user-contrib $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB) $(INSTALLSH) $(FULLCOQLIB) $(CONFIG) $(LINKCMO) $(GRAMMARCMA) - # reconstitute the list of core .cmi - $(INSTALLSH) $(FULLCOQLIB) $(CONFIG:.cmo=.cmi) \ - $(foreach lib,$(CORECMA:.cma=_MLLIB_DEPENDENCIES) $(PLUGINSCMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .cmi,$($(lib)))) + $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI) ifeq ($(BEST),opt) $(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB) $(INSTALLSH) $(FULLCOQLIB) $(CONFIG:.cmo=.cmx) $(CONFIG:.cmo=.o) $(LINKCMO:.cma=.cmxa) $(LINKCMO:.cma=.a) |
