diff options
| author | Hugo Herbelin | 2020-08-19 02:50:27 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-19 09:00:24 +0200 |
| commit | c3ff8bd78615c3f73a56d7a2dbfeea680f4163b6 (patch) | |
| tree | 35988d9e3687298a0c42a6b05bc3474493f325b7 /test-suite/Makefile | |
| parent | daed771ff18978dea536b277e00c0ca0149129ee (diff) | |
No more arithmetic directory test-suite.
The directory is obsolete since 7461fe4f.
Diffstat (limited to 'test-suite/Makefile')
| -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`; \ |