src/Tools/rm-logfiles
changeset 4578 9f79e84ce00d
parent 4577 674b0b354feb
child 4579 4f1e445b20d7
equal deleted inserted replaced
4577:674b0b354feb 4578:9f79e84ce00d
     1 #! /bin/sh
       
     2 # $Id$
       
     3 #Remove useless files from subdirectories
       
     4 
       
     5 find . \( -name log -o -name make\*.log\* -o -name test -o -name .\*.thy.ML \) -print \
       
     6   | xargs rm