| changeset 608 | 245633e2fd57 |
| parent 263 | d45f0af592f0 |
| child 820 | 11e4827b3d75 |
| 607:72fc777dbda0 | 608:245633e2fd57 |
|---|---|
1 #! /bin/sh |
1 #! /bin/sh |
2 #rm-logfiles: remove useless files from subdirectories |
2 #rm-logfiles: remove useless files from subdirectories |
3 rm log */make*.log */make*.log.gz |
3 rm log */make*.log */make*.log.gz |
4 rm */test |
4 rm */test |
5 rm */.*.thy.ML |
5 find . -name '.*.thy.ML' -print -exec rm {} \; |
6 rm */ex/.*.thy.ML |
|
7 rm HOL/Subst/.*.thy.ML |