On Wed, Aug 16, 2023 at 6:45 PM Etsuro Fujita <etsuro.fuj...@gmail.com> wrote: > On Wed, Aug 16, 2023 at 9:41 AM Richard Guo <guofengli...@gmail.com> wrote: > > On Tue, Aug 15, 2023 at 7:50 PM Etsuro Fujita <etsuro.fuj...@gmail.com> > > wrote: > >> So we should have modified the second one as well? Attached is a > >> small patch for that. > > > Agreed, nice catch! +1 to the patch. > > Thanks for looking!
Pushed. Best regards, Etsuro Fujita
