diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-27 12:02:18 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-27 12:02:18 +0100 |
| commit | f34946ecfb0ea2c75337369f3e41e9562be0d84b (patch) | |
| tree | b68e098e7ee85c6e1cc5f013c1ba9f7a736328e7 /test-suite/Makefile | |
| parent | 9182cdfba977eef23bd5a9db647c8227d87f59fc (diff) | |
include test-suite/coqchk in the summary log
Diffstat (limited to 'test-suite/Makefile')
| -rw-r--r-- | test-suite/Makefile | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 45a2e2046..d5adc4e5f 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -141,6 +141,7 @@ summary: $(call summary_dir, "STM tests", stm); \ $(call summary_dir, "IDE tests", ide); \ $(call summary_dir, "VI tests", vi); \ + $(call summary_dir, "Coqchk tests", coqchk); \ nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \ nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \ nb_tests=`expr $$nb_success + $$nb_failure`; \ |