build: add --htmldir option

Defaults to docdir but makes it possible to install html documentation
separately.

wscript

@@ -942,6 +942,7 @@ _INSTALL_DIRS_LIST = [
     ('datadir', '${PREFIX}/share',    'data files'),
     ('mandir',  '${DATADIR}/man',     'man pages '),
     ('docdir',  '${DATADIR}/doc/mpv', 'documentation files'),
+    ('htmldir', '${DOCDIR}',          'html documentation files'),
     ('zshdir',  '${DATADIR}/zsh/site-functions', 'zsh completion functions'),
 
     ('confloaddir', '${CONFDIR}', 'configuration files load directory'),

wscript_build.py

@@ -19,7 +19,7 @@ def _build_html(ctx):
         target       = 'DOCS/man/mpv.html',
         source       = 'DOCS/man/mpv.rst',
         rule         = '${RST2HTML} ${SRC} ${TGT}',
-        install_path = ctx.env.DOCDIR)
+        install_path = ctx.env.HTMLDIR)
 
     _add_rst_manual_dependencies(ctx)