aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Makefile.build2
1 files changed, 1 insertions, 1 deletions
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