diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 9 |
1 files changed, 3 insertions, 6 deletions
@@ -378,12 +378,9 @@ clean:: # tests ########################################################################### -check.log: world - cd test-suite; ./check -$(BEST) > check.log - -check:: check.log - cat check.log - grep -F 'Error!' check.log +check:: world + cd test-suite; ./check -$(BEST) | tee check.log + grep -F 'Error!' test-suite/check.log ########################################################################### # theories and states |