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 <[email protected]> * doc/texinfo.texi @code{@@settitle}): no title in the document anymore in the default case in HTML. It was redundant with the @top. -- Pat
