--- a/src/Tools/rm-logfiles Wed Jan 14 16:38:04 1998 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-#! /bin/sh
-# $Id$
-#Remove useless files from subdirectories
-
-find . \( -name log -o -name make\*.log\* -o -name test -o -name .\*.thy.ML \) -print \
- | xargs rm