| changeset 608 | 245633e2fd57 |
| parent 263 | d45f0af592f0 |
| child 820 | 11e4827b3d75 |
--- a/src/Tools/rm-logfiles Tue Sep 13 10:42:34 1994 +0200 +++ b/src/Tools/rm-logfiles Tue Sep 13 11:19:38 1994 +0200 @@ -2,6 +2,4 @@ #rm-logfiles: remove useless files from subdirectories rm log */make*.log */make*.log.gz rm */test -rm */.*.thy.ML -rm */ex/.*.thy.ML -rm HOL/Subst/.*.thy.ML +find . -name '.*.thy.ML' -print -exec rm {} \;