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