doc: Give users the freedom to use their own style in the HTML documentation

[Bruno Haible]

Hi José,

I always prefer to read documentation in HTML format. When reading the poke
documentation,

1) I was annoyed to have a white-text-on-black-background style, because it
   hurts the eyes in an otherwise black-text-on-white-background desktop.

2) I was even surprised to see that the doc I generate locally, as well as
   the doc a user can generate from the distributed tarballs [1], makes a
   network reference to www.jemarch.net when viewed for the first time.
   It gives the owner of that site (and every internet node operator on
   the way) the opportunity to get a notification when the user opens the
   documentation for the first time.

In fact, the AM_MAKEINFOHTMLFLAGS variable is not overridable by the user
(who can only give a MAKEINFOFLAGS as a 'configure' argument).

I would propose to give users
  - the default style by default,
  - the freedom to use their own style instead of yours.

Patch attached.

Bruno

[1] 
https://gitlab.com/gnu-poke/ci-distcheck/-/jobs/artifacts/master/raw/poke-snapshot.tar?job=check-optimized

0001-doc-Give-users-the-freedom-to-use-their-own-style-in.patch
Description: Text Data