On Tue, Aug 27, 2024 at 12:01 PM Thomas Munro <thomas(dot)munro(at)gmail(dot)com> wrote:
>
> Thanks! And that's great news. Do you want to report this experience
> to the PR, in support of committing it? That'd make it seem easier to
> consider shipping a back-ported copy...
Yes, I will do that.