Re: info.js demo on Texinfo manual updated on website

[Patrice Dumas]

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  <pertusus@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.

-- 
Pat