Updates following comments by Dave Gilbert.
commitb1fc9315368c2acf86cf3329da82852fc80fdc27
authorjay <jay>
Sat, 16 Jul 2005 18:58:05 +0000 (16 18:58 +0000)
committerjay <jay>
Sat, 16 Jul 2005 18:58:05 +0000 (16 18:58 +0000)
tree3aecc5ceb6256a88fc5e966ffc3ba35495a48e58
parent81d00af3e5d4756579ff06d7633dd7553842c230
Updates following comments by Dave Gilbert.
doc/find.texi