On Fri, Dec 6, 2019 at 5:27 PM Etsuro Fujita <etsuro(dot)fujita(at)gmail(dot)com> wrote:> If no objections, I'll push the patch.
Pushed. Thanks for the report, Alexander Lakhin!
Best regards,Etsuro Fujita