# HG changeset patch # User lcp # Date 793900739 -3600 # Node ID 26138063bb880e96f88d050db0a713da2bf14131 # Parent cc80f53b28c61446ca89d4208bf46a9ed6aa52a2 New shell script for finding orphan .ML files (those with no .thy file) diff -r cc80f53b28c6 -r 26138063bb88 src/Tools/find-orphans --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/find-orphans Mon Feb 27 16:58:59 1995 +0100 @@ -0,0 +1,6 @@ +#! /bin/csh +# $Id$ +# Find all "orphan" ML-files (those with no thy-file) +foreach f (*.ML) + if ( ! -f $f:r.thy ) echo $f +end