#! /bin/sh #rm-logfiles: remove useless files from subdirectories rm log */make*.log */make*.log.gz rm */test find . -name '.*.thy.ML' -print -exec rm {} \;