diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-05-31 16:52:38 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-05-31 16:52:38 +0200 |
| commit | 38d3aa91fb67767b9bd8aec4d14de3fd275e3c2c (patch) | |
| tree | 76163ddb739d50110ba93ce356f376c3652f171b /Makefile.build | |
| parent | 7c1b6714fe73c6cd8685bccef58eb6839a57fcb9 (diff) | |
Makefile.build: test-suite all = run + report, so don't report again
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index 8aedd9cec..f86dce9ab 100644 --- a/Makefile.build +++ b/Makefile.build @@ -454,7 +454,6 @@ check: validate test-suite test-suite: world $(ALLSTDLIB).v $(MAKE) $(MAKE_TSOPTS) clean $(MAKE) $(MAKE_TSOPTS) all - $(MAKE) $(MAKE_TSOPTS) report ########################################################################### # Default rules for compiling ML code |