From 5e9b37a815795efaafd64ab8fe19bf8560d70203 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 17 Apr 2016 12:29:51 +0200
Subject: Add plugins to Makefile.

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

diff --git a/Makefile.build b/Makefile.build
index fb6bfa87fe..b551242f6b 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)
+BEAUTIFIED=$(THEORIESVO) $(PLUGINSVO)
 TOBEAUTIFY=$(BEAUTIFIED:.vo=.v.beautified)
 
 check-beautify: $(TOBEAUTIFY)
-- 
cgit v1.2.3