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