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