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