On 11/18/22 15:48, Patrice Dumas wrote:
On Fri, Nov 18, 2022 at 03:19:23PM -0800, Per Bothner wrote:
Before, when I converted the DomTerm manual to html the output contained:
<h1 class="settitle">DomTerm - a terminal emulator and console using DOM and
JavaScript</h1>
This is now gone.
Looks a change in the generated html broke this.
Yes:
2022-03-11 Patrice Dumas <pertu...@free.fr>
* doc/texinfo.texi @code{@@settitle}): no title in the
document anymore in the default case in HTML.
It was redundant with the @top.
I'm not sure it is. There is no place in index.html that contains the actual
title
of the manual as a whole. I see:
<title>Top (GNU Texinfo 7.0)</title>
<meta name="description" content="Top (GNU Texinfo 7.0)">
<meta name="keywords" content="Top (GNU Texinfo 7.0)">
...
<h1 class="top" id="Texinfo">Texinfo</h1>
There are 3 places that *include* the title of manual: "Top (GNU Texinfo 7.0)"
However, doing pattern matching to extract the manual title seems losing,
especially if "Top" might be translated.
Note this was a compatility-breaking changes - it breaks people's
existing JavaScript or stylesheets.
--
--Per Bothner
p...@bothner.com http://per.bothner.com/
