diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-02 18:24:03 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-02 18:34:12 +0100 |
| commit | 6316e8b380a9942cd587f250eb4a69668e52019e (patch) | |
| tree | 00116e64de7adc858c56e751944f2ad7c43fe837 /Makefile.build | |
| parent | a80351f98adeada2b9219679de130e28c1b41479 (diff) | |
Adding a target report to test-suite's Makefile to get a short summary.
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 0455a247b..98ef81f38 100644 --- a/Makefile.build +++ b/Makefile.build @@ -494,7 +494,7 @@ check: validate test-suite test-suite: world $(ALLSTDLIB).v $(MAKE) $(MAKE_TSOPTS) clean $(MAKE) $(MAKE_TSOPTS) all - $(HIDE)if grep -F 'Error!' test-suite/summary.log ; then false; fi + $(MAKE) $(MAKE_TSOPTS) report ################################################################## # partial targets: 1) core ML parts |