Re: HTML <title> node names: Not emitting 'Top (Manual name)'

On Tue, Mar 12, 2024 at 01:14:19PM +0100, Arsen Arsenović wrote:
> Hello,
> 
> Currently, makeinfo generates HTML <title> elements that contain a node
> name.  This is good.  However, for the top node, emitting the title name
> is redundant, and should likely be replaced with simply the manual name
> (since the node name 'Top' is uninteresting).
> 
> Specifically, in the example of
> https://www.aarsen.me/~arsen/gcc/ST/gcc.html/ the HTML title is 'Top
> (Using the GNU Compiler Collection)' rather than just simply 'Using the
> GNU Compiler Collection'.  This behavior is desirable on all other nodes
> (e.g. https://www.aarsen.me/~arsen/gcc/ST/gcc.html/Solaris-2-Options.html
> being titled Solaris 2 Options (Using the GNU Compiler Collection
> (GCC))) is good.
> 
> Is there a way to achieve this?
> 
> TIA, have a lovely day.

It seems like a good idea, does anybody have any opposition to making
this change?