diff options
| author | Hugo Herbelin | 2016-04-17 12:29:51 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 21:55:49 +0200 |
| commit | 5e9b37a815795efaafd64ab8fe19bf8560d70203 (patch) | |
| tree | 46a7a0cd533c78908ff1bb43ecd859b016d73a41 | |
| parent | 834885cb8cbc4d6924a63b898c7a5a32cfd0211c (diff) | |
Add plugins to Makefile.
| -rw-r--r-- | Makefile.build | 2 |
1 files changed, 1 insertions, 1 deletions
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) |