On Thu, Mar 14, 2024 at 10:34:00PM +0100, Arsen Arsenović wrote: > > By all means, if changing the page title for the Top node causes > > significant problems, we can avoid making this change. But it is > > hard to imagine why it would cause a problem. > > > > I don't mind avoiding this time for the time being, if it is felt > > there has been a lot of change to the HTML output recently. Once > > things settle down, we could revisit this. > > This could be a customization variable or such in the meanwhile too.
I do not think that it is probelmatic to change if it is better. I think that the Top () conveys some information, although not very much, both would be ok for me. It is easier to explain what is done if we keep the Top, though. As for adding a customization variable, I do not think that such a variation in formatting is worth a customization variable, however something that could be considered is a customization variable for the HTML title of the Top/first file in a split manual. -- Pat