| 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 |