# 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