src/Tools/agrep

--- a/src/Tools/agrep	Fri Feb 16 17:24:51 1996 +0100
+++ b/src/Tools/agrep	Fri Feb 16 18:00:47 1996 +0100
@@ -1,2 +1,2 @@
 #! /bin/csh
-grep "$*" {Pure/Syntax,Pure/Thy}/*ML */*ML */*/*ML 
+grep "$*" */*.ML */*/*.ML