> On Mon, Mar 20, 2023 at 10:31:14AM +0100, Tomas Vondra wrote:
>
> On 3/17/23 21:20, Dmitry Dolgov wrote:
> >> ...
> >
> > It occurred to me this fix wasn't applied yet, right? Are there any
> > concerns about it?
>
> Thanks for reminding me, I had it on the back burner. I added a trivial
> regression test, polished the commit message a bit and pushed it
> (including backpatching).
Great, thank you.
