src/Tools/agrep

--- a/src/Tools/agrep	Tue Sep 30 16:12:38 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-#! /bin/csh
-grep "$*" */*.ML */*/*.ML TFL/*.sml TFL/*.sig TFL/examples/Subst/*.ML
-