Fix last change for docs search procedure (suggested by Dave Love).
commit3085f862f5ececc01be627cd3a37b6cd51aa9405
authorEli Zaretskii <eliz@gnu.org>
Tue, 10 Oct 2000 12:46:32 +0000 (10 12:46 +0000)
committerEli Zaretskii <eliz@gnu.org>
Tue, 10 Oct 2000 12:46:32 +0000 (10 12:46 +0000)
tree8df9132bed4c7c4351802e4cc4d16177351d6e1f
parentb40bfb99b0238b6a0b3fc15d231899d68e7231e3
Fix last change for docs search procedure (suggested by Dave Love).
man/help.texi