summaryrefslogtreecommitdiff
path: root/otherlibs/Makefile
diff options
context:
space:
mode:
authorhendriktews <hendrik@askra.de>2016-10-21 16:40:14 +0200
committerDamien Doligez <damien.doligez@gmail.com>2016-10-21 16:40:14 +0200
commit0bb16e093449a4016acc58718c5affb63cbce330 (patch)
tree60464984926e0c1ac6d867cc27fbf5def9aa0f95 /otherlibs/Makefile
parent3e8a4a6de48e1422efb93b3ee0b85ec0d1107c0a (diff)
downloadocaml-0bb16e093449a4016acc58718c5affb63cbce330.tar.gz
improve installation of additional material (#827)
- install missing mli and cmti files for compiler-libs and otherlibs - new make target install-compiler-sources to install compiler-libs ml files
Diffstat (limited to 'otherlibs/Makefile')
-rw-r--r--otherlibs/Makefile3
1 files changed, 2 insertions, 1 deletions
diff --git a/otherlibs/Makefile b/otherlibs/Makefile
index 4758bf599e..05a093fd07 100644
--- a/otherlibs/Makefile
+++ b/otherlibs/Makefile
@@ -84,7 +84,8 @@ install::
cp dll$(CLIBNAME)$(EXT_DLL) "$(INSTALL_STUBLIBDIR)/"; fi
cp lib$(CLIBNAME).$(A) "$(INSTALL_LIBDIR)/"
cd "$(INSTALL_LIBDIR)"; $(RANLIB) lib$(CLIBNAME).$(A)
- cp $(LIBNAME).cma $(CMIFILES) $(CMIFILES:.cmi=.mli) "$(INSTALL_LIBDIR)/"
+ cp $(LIBNAME).cma $(CMIFILES) $(CMIFILES:.cmi=.mli) \
+ $(CMIFILES:.cmi=.cmti) "$(INSTALL_LIBDIR)/"
if test -n "$(HEADERS)"; then \
cp $(HEADERS) "$(INSTALL_LIBDIR)/caml/"; fi