From c3ff8bd78615c3f73a56d7a2dbfeea680f4163b6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 19 Aug 2020 02:50:27 +0200
Subject: No more arithmetic directory test-suite.

The directory is obsolete since 7461fe4f.
---
 test-suite/Makefile | 1 -
 1 file changed, 1 deletion(-)

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`; \
-- 
cgit v1.2.3