1 #! /bin/sh
2 #rm-logfiles: remove useless files from subdirectories
3 rm log */make*.log */make*.log.gz */make*.log.z
4 rm */test
5 rm */.*.thy.ML
6 rm */ex/.*.thy.ML
7 rm HOL/Subst/.*.thy.ML