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