On Tue, Nov 21, 2023 at 10:41:10AM -0500, Marek Polacek wrote: > On Mon, Nov 20, 2023 at 05:32:47PM +0100, Jakub Jelinek wrote: > > LGTM. > > Thanks a lot. Since Richi seems to be fine with the patch as well, > I'll push it tomorrow AM if no comments.
Pushed. I'll update changes.html now. Thanks to everybody who contributed to this effort! Marek
