--- a/src/Tools/agrep Fri Jan 03 10:45:31 1997 +0100 +++ b/src/Tools/agrep Fri Jan 03 10:48:28 1997 +0100 @@ -1,2 +1,3 @@ #! /bin/csh -grep "$*" */*.ML */*/*.ML +grep "$*" */*.ML */*/*.ML TFL/*.sml TFL/*.sig TFL/examples/Subst/*.ML +