--- a/rm-logfiles Wed Jul 19 15:53:43 1995 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,5 +0,0 @@
-#! /bin/sh
-#rm-logfiles: remove useless files from subdirectories
-rm log */make*.log */make*.log.gz
-rm */test
-find . -name '.*.thy.ML' -print -exec rm {} \;