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-6d5037567...@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
