From b0210638366d6584b709496b0f0eeeecb17c3fae Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 11 Oct 2019 13:43:20 +0200
Subject: [make] separate generated gramlib ml files from mli files (fix
 #10864)

---
 Makefile.install | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Makefile.install')

diff --git a/Makefile.install b/Makefile.install
index 608e8a3c8e..456c391fd9 100644
--- a/Makefile.install
+++ b/Makefile.install
@@ -92,13 +92,13 @@ install-tools:
 
 INSTALLCMI = $(sort \
 	$(filter-out checker/% ide/% tools/%, $(MLIFILES:.mli=.cmi)) \
-	$(filter %.cmi, $(GRAMMLFILES:.mli=.cmi)) gramlib/.pack/gramlib.cmi \
+	$(GRAMMLIFILES:.mli=.cmi) gramlib/.pack/gramlib.cmi \
 	$(foreach lib,$(CORECMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES))))) \
 	$(PLUGINS:.cmo=.cmi)
 
 INSTALLCMX = $(sort $(filter-out checker/% ide/% tools/% dev/% \
 	configure.cmx toplevel/coqtop_byte_bin.cmx plugins/extraction/big.cmx, \
-	$(filter %.cmx, $(GRAMMLFILES:.ml=.cmx)) $(MLFILES:.ml=.cmx)))
+	$(GRAMMLFILES:.ml=.cmx) $(MLFILES:.ml=.cmx)))
 
 install-devfiles:
 	$(MKDIR) $(FULLBINDIR)
-- 
cgit v1.2.3