aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--Makefile1
-rwxr-xr-xtest-suite/check7
2 files changed, 0 insertions, 8 deletions
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