#! /bin/sh # $Id$ #Remove useless files from subdirectories rm log */make*.log */make*.log.gz rm */test rm */.*.thy.ML */*/.*.thy.ML