From 25462addaf604ff51e886bbc92937bb272982b04 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 13 Jun 2017 19:33:44 +0200
Subject: Makefile.build: do *not* build PLUGINSCMO by default (followup of PR
 #709)

---
 Makefile.build | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile.build b/Makefile.build
index 6e048ce94d..8c6f546de1 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -606,7 +606,7 @@ OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack
 coqlib: theories plugins
 
 theories: $(THEORIESVO)
-plugins: $(PLUGINSVO) $(PLUGINSCMO)
+plugins: $(PLUGINSVO)
 
 .PHONY: coqlib theories plugins
 
-- 
cgit v1.2.3