# HG changeset patch # User paulson # Date 852284908 -3600 # Node ID 428efffe8599eedb71fbd6bd2756b0ff0a42db7e # Parent 357adb429fda3166565f8daefc0f4f151c6f3271 Added TFL diff -r 357adb429fda -r 428efffe8599 src/Tools/agrep --- 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 +