# HG changeset patch
# User lcp
# Date 760292200 -3600
# Node ID d45f0af592f02aa9fe9043dd70fa04ecc48e661e
# Parent  024b242bc26f758bbf2d109bb5494f3781214500
no longer removes *.z

diff -r 024b242bc26f -r d45f0af592f0 rm-logfiles
--- a/rm-logfiles	Thu Feb 03 16:06:55 1994 +0100
+++ b/rm-logfiles	Thu Feb 03 17:16:40 1994 +0100
@@ -1,6 +1,6 @@
 #! /bin/sh
 #rm-logfiles: remove useless files from subdirectories
-rm log */make*.log */make*.log.gz */make*.log.z
+rm log */make*.log */make*.log.gz
 rm */test
 rm */.*.thy.ML
 rm */ex/.*.thy.ML
diff -r 024b242bc26f -r d45f0af592f0 src/Tools/rm-logfiles
--- a/src/Tools/rm-logfiles	Thu Feb 03 16:06:55 1994 +0100
+++ b/src/Tools/rm-logfiles	Thu Feb 03 17:16:40 1994 +0100
@@ -1,6 +1,6 @@
 #! /bin/sh
 #rm-logfiles: remove useless files from subdirectories
-rm log */make*.log */make*.log.gz */make*.log.z
+rm log */make*.log */make*.log.gz
 rm */test
 rm */.*.thy.ML
 rm */ex/.*.thy.ML