diff options
| author | coqbot | 2020-08-24 13:45:14 +0200 |
|---|---|---|
| committer | GitHub | 2020-08-24 13:45:14 +0200 |
| commit | 99e944f873589cf350e49f3bfda6094ffbfa545b (patch) | |
| tree | cb4c0b04c5a776db2a5f84c496d75e762a558267 | |
| parent | 59f383ad7f460b9a4a438fb7b84f8c071f960351 (diff) | |
| parent | c3ff8bd78615c3f73a56d7a2dbfeea680f4163b6 (diff) | |
Merge PR #12854: Mini-fix in test suite: arithmetic directory does no longer exist
Reviewed-by: SkySkimmer
| -rw-r--r-- | test-suite/Makefile | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index f7447d6cec..7d219b6e8b 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -198,7 +198,6 @@ summary: $(call summary_dir, "Coqdoc tests", coqdoc); \ $(call summary_dir, "tools/ tests", tools); \ $(call summary_dir, "Unit tests", unit-tests); \ - $(call summary_dir, "Machine arithmetic tests", arithmetic); \ $(call summary_dir, "Ltac2 tests", ltac2); \ 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`; \ |