| changeset 820 | 11e4827b3d75 |
| parent 608 | 245633e2fd57 |
| child 2161 | c25714ca1c19 |
--- a/src/Tools/rm-logfiles Wed Dec 21 13:26:26 1994 +0100 +++ b/src/Tools/rm-logfiles Wed Dec 21 13:36:02 1994 +0100 @@ -1,5 +1,6 @@ #! /bin/sh -#rm-logfiles: remove useless files from subdirectories +# $Id$ +#Remove useless files from subdirectories rm log */make*.log */make*.log.gz rm */test find . -name '.*.thy.ML' -print -exec rm {} \;