--- a/src/Tools/agrep Fri Nov 18 13:14:23 1994 +0100 +++ b/src/Tools/agrep Mon Nov 21 10:39:32 1994 +0100 @@ -1,2 +1,2 @@ #! /bin/csh -grep "$*" {Pure/Syntax,Pure/Thy}/*ML */*ML */ex/*ML +grep "$*" {Pure/Syntax,Pure/Thy}/*ML */*ML */*/*ML