check-doc: add an option to ignore some explicit options from the command's help

check-doc: add an option to ignore some explicit options from the command's help

There are a few rare cases where some options listed in the program's
built-in help page may not be documented for a valid reason. This patch
provides an option to the checking script to not complain about them, but:

 - the listed options must include a comment about why, to ensure that the
user thinks twice about it and because it is better for maintainability;

 - the listed option must be part of the options listed by the application
to ensure the command line invocation of the script will remain up to date.

This new option is then used for the check of the "configure" options
because for a few of them the right place to document them is in the
INSTALL file provided by Autoconf and not in our Window Maker specific doc.

Signed-off-by: Christophe CURIS <christophe.curis@free.fr>