# HG changeset patch
# User wenzelm
# Date 882272231 -3600
# Node ID 16b92885de6bc1b9eb7c9cd815cadda6226cb53a
# Parent  950001e4859ac53ad6b70c11e93ad8fd2a1ab5ed
obsolete;

diff -r 950001e4859a -r 16b92885de6b src/Tools/find-orphans
--- a/src/Tools/find-orphans	Tue Dec 16 12:24:31 1997 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-#! /bin/csh
-# $Id$
-# Find all "orphan" ML-files (those with no thy-file)
-foreach f (*.ML)
-  if ( ! -f $f:r.thy ) echo $f
-end