diff options
| -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`; \ |