rm-logfiles
author clasohm
Wed, 06 Oct 1993 14:45:04 +0100
changeset 34 747f1aad03cf
parent 0 a5a9c433f639
child 263 d45f0af592f0
permissions -rwxr-xr-x
changed filenames to lower case name of theory the file contains (only one theory per file, therefore llist.ML has been split)

#! /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