Docs: merge the two Texi2HTML init files

Docs: merge the two Texi2HTML init files

Formatting for the web site is enabled through "-D web_manual"Texinfo
command line option.

Cherry-picked, squashed together by John from commits in
dev/gperciva branch:
86dd84e0ed4248e931ce6998ac94de4bd9969809
89ba33490b1dd18b69a4fcb98fea70b69841aece
8dd8d653cb43bc6b86ac014b022f9834695b24f5
f1ecf05f6b816e7f2e890a01c1f862f99f2092e9
e3fbdebeac091b8be5d1d4b186f3cdaf9aa50fdb

In addition to this merging, John made a few subsequent changes:

- use --split=subsubsection for the website, which makes
extract_texi_filenames.py generate a correct map;

- reorder Texi2HTML command line arguments to make sure the init file
catches the ones which are necessary;

- splitted HTML docs: downcase all filenames (manuals and web site),
and sections anchors (which fix the duplicate anchors issues that
makes Opera barf);

- fix translated docs map files loading.