Provided by: dejagnu_1.6.3-1_all bug

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
       -v, --verbose  Emit additional output describing the operation of dejagnu help itself.

       -w, --path     This option is simply passed on to man.

       -W             This option is simply passed on to man.


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
       man(1)


AUTHORS
       Jacob Bachmeyer


BUGS
       Currently only supports man pages.

GNU                                             December 19, 2018                                DEJAGNU-HELP(1)