On Tue, Mar 30, 2021 at 8:40 PM Etsuro Fujita <etsuro(dot)fujita(at)gmail(dot)com> wrote:> I'm happy with the patch, so I'll commit it if there are no objections.
Pushed.
Best regards,Etsuro Fujita