debian/rules: skip html generation when DEB_BUILD_OPTIONS=nodoc
Debian policy 4.9.1 explains:
nodoc
This tag says to skip any build steps that only
generate package documentation. Files required by
other sections of Debian Policy, such as copyright and
changelog files, must still be generated and put in
the package, but other generated documentation such as
help2man-generated pages, Doxygen-generated API
documentation, or info pages generated from Texinfo
sources should be skipped if possible. This option
does not change the set of binary packages generated
by the source package, but documentation-only binary
packages may be nearly empty when built with this
option.
For now this will only affect HTML documentation, not the man pages in
git-man, since those are needed for 'git <command> --help' to work.
Tested by running "DEB_BUILD_OPTIONS=nodoc fakeroot debian/rules binary"
and examining the result.
Signed-off-by: Jonathan Nieder <jrnieder@gmail.com>