rm-logfiles

Local version of (original) hypsubst: needs no simplifier

+
−#! /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 {} \;