DEJAGNU-HELP(1) | General Commands Manual (urm) | DEJAGNU-HELP(1) |
dejagnu help
—
display manual pages for DejaGnu auxiliary
commands
dejagnu help |
[options...] ⟨command⟩ |
The dejagnu help
command displays
long-form documentation for DejaGnu auxiliary commands.
The dejagnu help
command checks for
man pages in a doc/ directory next to the
commands/ directory where this script is located. If
the page is found there, a full file name is given to
man
. Otherwise, only the command name is given and
the search described in man(1) is performed.
Jacob Bachmeyer
Currently only supports man pages.
December 19, 2018 | GNU |