rm-logfiles
author lcp
Fri Apr 15 18:34:26 1994 +0200 (1994-04-15)
changeset 328 2d1b460dbb62
parent 263 d45f0af592f0
child 608 245633e2fd57
permissions -rwxr-xr-x
penultimate Springer draft
     1 #! /bin/sh
     2 #rm-logfiles: remove useless files from subdirectories
     3 rm log */make*.log */make*.log.gz
     4 rm */test
     5 rm */.*.thy.ML
     6 rm */ex/.*.thy.ML
     7 rm HOL/Subst/.*.thy.ML