aboutsummaryrefslogtreecommitdiff
path: root/Makefile.build
diff options
context:
space:
mode:
authorletouzey2011-12-08 17:34:44 +0000
committerletouzey2011-12-08 17:34:44 +0000
commit61c090d3e5779996c32a9314abe08592df434c30 (patch)
treeef0116d0d12d1c9e8863d47d5dafc007b4b2c49f /Makefile.build
parent8b3e22ced65c9393b19a2d6b3184d72ae8c32981 (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.build12
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)