| changeset 263 | d45f0af592f0 |
| parent 0 | a5a9c433f639 |
| child 608 | 245633e2fd57 |
--- 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