separate build targets for man and html documentation

separate build targets for man and html documentation

This introduces new build targets "man" and "html" which allow building
the documentation in the respective formats separately. This helps
people with a partial documentation build chain: html pages can be built
without xmlto.

This is documented in INSTALL now, together with corrections: Before,
instructions in INSTALL would build man+html but install man only. Now
the instructions build and install both, and new and pre-existing
targets are explained.

Note that build targets "doc" and "man" correspond to install targets
"install-doc install-html" and "install-doc" respectively. This
inconsistency is not changed, in order to keep everyone's build scripts
from breaking.

Signed-off-by: Michael J Gruber <michaeljgruber+gmane@fastmail.fm>
Signed-off-by: Junio C Hamano <gitster@pobox.com>