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

[Patrice Dumas]

On Sun, Mar 12, 2023 at 11:43:27AM +0000, Gavin Smith wrote:
> On Sun, Mar 12, 2023 at 11:49:38AM +0100, Patrice Dumas wrote:
> > On Sat, Mar 11, 2023 at 12:01:18PM +0100, Arsen Arsenović wrote:
> > > 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.
> > 
> > I think that the best would be, after having decided on a default, to
> > have the alternative order specified in CONTENTS_OUTPUT_LOCATION.  So,
> > for example if it is shortcontents first and contents next in the
> > default case, there would be both CONTENTS_OUTPUT_LOCATION=after_top
> > and CONTENTS_OUTPUT_LOCATION=after_top_short_last to be able to specify
> > that.
> 
> I agree with Arsen that the shortcontents should come first.  I don't
> care if other options are added too to swap the orders.

Ok. Let's wait for users to ask for the other order to add the
CONTENTS_OUTPUT_LOCATION possibilities.

-- 
Pat