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