On Mon, Aug 28, 2023 at 01:20:32AM +0000, Michael wrote: > > Did I miss something or was the Wiki page just not updated? :-) > The wiki's outdated. A tool generates the content, but actually updating the wiki involves a manual copy & paste. I'll get it updated. noah