From f104dffa7661999bbbf405c2b0bb654758678bc6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 27 Apr 2016 22:13:02 +0200
Subject: Revert "Add plugins to Makefile."

This reverts commit 5e9b37a815795efaafd64ab8fe19bf8560d70203.
---
 Makefile.build | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile.build b/Makefile.build
index b551242f6b..fb6bfa87fe 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -498,7 +498,7 @@ test-suite: world $(ALLSTDLIB).v
 	$(MAKE) $(MAKE_TSOPTS) all
 	$(MAKE) $(MAKE_TSOPTS) report
 
-BEAUTIFIED=$(THEORIESVO) $(PLUGINSVO)
+BEAUTIFIED=$(THEORIESVO)
 TOBEAUTIFY=$(BEAUTIFIED:.vo=.v.beautified)
 
 check-beautify: $(TOBEAUTIFY)
-- 
cgit v1.2.3