From 31eead537632931d44d31f55905a277d7e5b1624 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Fri, 24 Jun 2016 13:33:07 +0200 Subject: Makefile.install: fix a typo in last commit c954bb5, sorry --- Makefile.install | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile.install b/Makefile.install index 09c3331f0..4dad8cf0d 100644 --- a/Makefile.install +++ b/Makefile.install @@ -87,7 +87,7 @@ install-tools: INSTALLCMI = $(sort \ $(filter-out checker/% ide/% tools/%, $(MLIFILES:.mli=.cmi)) \ $(foreach lib,$(CORECMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES))))) \ - $(PLUGINS:.cmo:.cmi) + $(PLUGINS:.cmo=.cmi) install-devfiles: $(MKDIR) $(FULLBINDIR) -- cgit v1.2.3