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). -- Joseph S. Myers jos...@codesourcery.com
