+−#! /bin/sh +−#rm-logfiles: remove useless files from subdirectories +−rm log */make*.log */make*.log.gz +−rm */test +−rm */.*.thy.ML +−rm */ex/.*.thy.ML +−rm HOL/Subst/.*.thy.ML