# HG changeset patch
# User wenzelm
# Date 884869078 -3600
# Node ID 9f79e84ce00deeec5115c31d657c5c5ee2911251
# Parent  674b0b354febe555f1cd41d633ad015d669e11c2
obsolete;

diff -r 674b0b354feb -r 9f79e84ce00d src/Tools/rm-logfiles
--- 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