Option to include man pages in documentation

Option to include man pages in documentation

Before this patch, HTML versions of man pages (man/*.rst) were already
built. However, since they are separate from the normal documentation,
their content is not indexed for Sphinx' search functionality.
Additionally it would simply be nice to have everything in one place.

To this end a new configure-time option is added to enable the inclusion
of man pages into the documentation. A dedicated option is necessary to
still be able to provide a static documentation build in the tarball
(not including man pages) as man pages contain build-specific paths and
values. The documentation with man pages is written to the directory
“doc/man-html”.

A future patch will extend Sphinx to link occurences of “:manpage:`…`”
to these man pages.

Signed-off-by: Michael Hanselmann <hansmi@google.com>
Reviewed-by: Guido Trotter <ultrotter@google.com>