Sandra Loosemore <sandra.loosemore@siemens.com> writes:

> On 3/9/23 13:38, Arsen Arsenović wrote:
>> Found the change.  HTML got support for CONTENTS_OUTPUT_LOCATION,
>> which defaults to after_top, which ignores the inline location of
>> these elements.  Here's a patch:
>> maintainer-scripts/ChangeLog:
>> 	* update_web_docs_git: Set CONTENTS_OUTPUT_LOCATION=inline in
>> 	order to put @shortcontents above contents. See
>> 	9dd976a4-4e09-d901-b949-6d5037567b9b@codesourcery.com on
>> 	gcc-patches.
>
> I don't think this is an adequate fix.  We mere mortals build the manuals with
> "make html" etc instead of the maintainer scripts for the web site, so we need
> a solution that we can put either in the Makefile or directly in the .texi
> files, that won't blow up for older versions of Texinfo that don't support this
> thing.
>
> -Sandra

OK, changed up a bit, what do you think of this: