src/Tools/agrep
changeset 2468 428efffe8599
parent 1512 ce37c64244c0
equal deleted inserted replaced
2467:357adb429fda 2468:428efffe8599
     1 #! /bin/csh
     1 #! /bin/csh
     2 grep "$*" */*.ML */*/*.ML 
     2 grep "$*" */*.ML */*/*.ML TFL/*.sml TFL/*.sig TFL/examples/Subst/*.ML
       
     3