author | paulson |
Tue, 05 Nov 1996 11:48:09 +0100 | |
changeset 2161 | c25714ca1c19 |
parent 2160 | ad4382e546fc |
child 2162 | f53171d7f86c |
--- a/src/Tools/rm-logfiles Tue Nov 05 11:20:52 1996 +0100 +++ b/src/Tools/rm-logfiles Tue Nov 05 11:48:09 1996 +0100 @@ -3,4 +3,4 @@ #Remove useless files from subdirectories rm log */make*.log */make*.log.gz rm */test -find . -name '.*.thy.ML' -print -exec rm {} \; +rm */.*.thy.ML */.*.thy.ML */*/.*.thy.ML