On Wed, 2023-02-01 at 09:33 -0500, Stefan Monnier wrote:
> > > Yes, please,
> > Done, thoughts?
> 
> I think we can go with that for now.  I'll try to fix the todo at
> some
> point, but I'm short on time for now,
> 
> 
>         Stefan
> 

Sure. Do we need to install this to the release branch? The bug doesn't
really break anything AFAIK, so I dont think it's really a release
blocker.

-- 
Vibhav Pant
vibhavp@gmail.com
GPG: 7ED1 D48C 513C A024 BE3A  785F E3FB 28CB 6AB5 9598