On Thursday, 22 September 2022 at 20:26:37 UTC, Paul Backus wrote: > Of course, with the planned migration to GitHub issues, all of > this discussion is somewhat moot. My last understanding was that this migration is *not* desired. If it really is, cool.