| changeset 2161 | c25714ca1c19 |
| parent 820 | 11e4827b3d75 |
| child 2168 | fcf18ada8904 |
| 2160:ad4382e546fc | 2161:c25714ca1c19 |
|---|---|
1 #! /bin/sh |
1 #! /bin/sh |
2 # $Id$ |
2 # $Id$ |
3 #Remove useless files from subdirectories |
3 #Remove useless files from subdirectories |
4 rm log */make*.log */make*.log.gz |
4 rm log */make*.log */make*.log.gz |
5 rm */test |
5 rm */test |
6 find . -name '.*.thy.ML' -print -exec rm {} \; |
6 rm */.*.thy.ML */.*.thy.ML */*/.*.thy.ML |