Joseph Myers <joseph@codesourcery.com> writes:

> On Mon, 20 Mar 2023, Sandra Loosemore wrote:
>
>> Joseph, could you maybe review the last piece?  A direct pointer to it in
>> Arsen's git is
>> 
>> https://git.sr.ht/~arsen/gcc/commit/bc734311cbca1085a1728f79b7eebef8cc7aeac3
>
> That's OK, assuming I understand correctly that makeinfo will still 
> succeed with a warning when it's an older version (gcc.gnu.org, where 
> update_web_docs_git runs, has version 6.5).

It should, yes, but I'd like to ask for that server to be updated to
Texinfo straight from the press (the press is currently at commit
e2d30b1270deacf5a1eab1d383733a5a088827d6).  Mark told me that this needs
approval from the GCC admins to do.

The reason for this is that the in-dev versions of Texinfo produce more
accessible HTML documentation due to a few changes that I've
incorporated into them, as well as a few made by the Texinfo
maintainers.

Do you think that would be OK?

Thanks, have a lovely night.
-- 
Arsen Arsenović