DEJAGNU-HELP(1) | General Commands Manual (urm) | DEJAGNU-HELP(1) |
NAME¶
dejagnu help
—
display manual pages for DejaGnu auxiliary
commands
SYNOPSIS¶
dejagnu help |
[options...] ⟨command⟩ |
DESCRIPTION¶
The dejagnu help
command displays
long-form documentation for DejaGnu auxiliary commands.
OPTIONS¶
FILES¶
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.
SEE ALSO¶
AUTHORS¶
Jacob Bachmeyer
BUGS¶
Currently only supports man pages.
December 19, 2018 | GNU |