From 0600dfc4b341c16625b1e17f598b1c3fbec12ea7 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
Date: Fri, 18 May 2018 15:41:41 +0200
Subject: Clean-up dead file in test-suite.

---
 Makefile         | 1 -
 test-suite/check | 7 -------
 2 files changed, 8 deletions(-)
 delete mode 100755 test-suite/check

diff --git a/Makefile b/Makefile
index f914de5a6..4db0d37a2 100644
--- a/Makefile
+++ b/Makefile
@@ -219,7 +219,6 @@ indepclean:
 	rm -f */*.pp[iox] plugins/*/*.pp[iox]
 	rm -rf $(SOURCEDOCDIR)
 	rm -f toplevel/mltop.byteml toplevel/mltop.optml
-	rm -f test-suite/check.log
 	rm -f glob.dump
 	rm -f config/revision.ml revision
 	rm -f plugins/micromega/.micromega.ml.generated
diff --git a/test-suite/check b/test-suite/check
deleted file mode 100755
index 3d14f6bc0..000000000
--- a/test-suite/check
+++ /dev/null
@@ -1,7 +0,0 @@
-#!/bin/sh
-
-MAKE="${MAKE:=make}"
-
-${MAKE} clean > /dev/null 2>&1
-${MAKE} all > /dev/null 2>&1
-cat summary.log
-- 
cgit v1.2.3