On Wed, Nov 6, 2024 at 11:06 PM Ashutosh Bapat <ashutosh.bapat....@gmail.com> wrote: > On Wed, Nov 6, 2024 at 4:10 PM Richard Guo <guofengli...@gmail.com> wrote: > > I intend to push this patch shortly, barring any objections, so that > > it can catch up with the next minor release (Nov. 14). > > I didn't get time to respond to your email and create a patch based on > my proposal. Sorry. I may not get time for another week or so. Please > feel free to push the patch, if you feel that it's in a committable > state.
Pushed with some tweaks to the commit message. Thanks Richard
