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