obsolete;
authorwenzelm
Tue, 16 Dec 1997 12:37:11 +0100
changeset 4420 16b92885de6b
parent 4419 950001e4859a
child 4421 88639289be39
obsolete;
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