diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 22:13:02 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 22:13:02 +0200 |
commit | f104dffa7661999bbbf405c2b0bb654758678bc6 (patch) | |
tree | e6865d1a1bcceaf489ecfaa5a8e548efdefa31fc /Makefile.build | |
parent | 2e0c91f19130cc87def012d8bf5aa78a8215d000 (diff) |
Revert "Add plugins to Makefile."
This reverts commit 5e9b37a815795efaafd64ab8fe19bf8560d70203.
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 b551242f6..fb6bfa87f 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) |