On Sat, 14 Jun 2025 at 19:04, David Rowley <dgrowle...@gmail.com> wrote:
> I propose I just push the fix_idea.patch and leave it at that for v18.
>
> Does anyone have any other ideas?

I've now pushed that as a fix.

David


Reply via email to