Should @shortcontents come before @contents with CONTENTS_OUTPUT_LOCATION=after_top?

[Arsen Arsenović]

Hi,

Currently, CONTENTS_OUTPUT_LOCATION=after_top outputs contents first,
then shortcontents, as is written in HTML.pm:4113.  Some manuals, such
as that of GCC, place @shortcontents first, in order to let the user
browse a briefer high-level overview before jumping into the (quite
large) table of contents.

Do you think this rationale makes sense, and should we output
@shortcontents first with after_top?  Alternatively, maybe we could
record the relative location of the contents commands in the document
and base ordering on that?

What do you think?

Thanks in advance.
-- 
Arsen Arsenović

signature.asc
Description: PGP signature