rm-logfiles
author nipkow
Tue May 09 22:10:08 1995 +0200 (1995-05-09)
changeset 1114 c8dfb56a7e95
parent 608 245633e2fd57
permissions -rwxr-xr-x
Prod is now a parent of Lfp.
Added thm induct2 to Lfp.
Changed the way patterns in abstractions are pretty printed.
It has become simpler now but fails if split has more than one argument
because then the ast-translation does not match.
     1 #! /bin/sh
     2 #rm-logfiles: remove useless files from subdirectories
     3 rm log */make*.log */make*.log.gz
     4 rm */test
     5 find . -name '.*.thy.ML' -print -exec rm {} \;