Re: use directly section childs with sectiontoc, set USE_NODES 0 for HTML

[Gavin Smith]

On Sun, Nov 01, 2020 at 07:26:52PM +0100, Patrice Dumas wrote:
> On Sun, Nov 01, 2020 at 11:40:56AM +0000, Gavin Smith wrote:
> > On Sun, Nov 01, 2020 at 01:37:04AM +0100, Patrice Dumas wrote:
> > > Hello,
> > > 
> > > Why is there no sectiontoc for the @top?
> > 
> > Because the index.html file usually has @contents or @shortcontents
> > as well as the Top node.
> > 
> > At https://www.gnu.org/software/texinfo/manual/texinfo/html_node/index.html
> > there are actually three tables of contents: @shortcontents, @contents,
> > and the menu.  This is unnecessary.
> 
> Ok, but then this means that there should be a sectiontoc if there is no
> @shortcontents nor @contents.

Yes, I agree.  Also, I wonder if the contents and shortcontents should
be output after the Top node in index.html, rather than before.