| changeset 2168 | fcf18ada8904 |
| parent 2161 | c25714ca1c19 |
| child 2955 | 92599a47a7ab |
| 2167:5819e85ad261 | 2168:fcf18ada8904 |
|---|---|
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 rm */.*.thy.ML */.*.thy.ML */*/.*.thy.ML |
6 rm */.*.thy.ML */*/.*.thy.ML |