| changeset 263 | d45f0af592f0 |
| parent 0 | a5a9c433f639 |
| child 608 | 245633e2fd57 |
| 262:024b242bc26f | 263:d45f0af592f0 |
|---|---|
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 */make*.log.z |
3 rm log */make*.log */make*.log.gz |
4 rm */test |
4 rm */test |
5 rm */.*.thy.ML |
5 rm */.*.thy.ML |
6 rm */ex/.*.thy.ML |
6 rm */ex/.*.thy.ML |
7 rm HOL/Subst/.*.thy.ML |
7 rm HOL/Subst/.*.thy.ML |