On Fri, Sep 21, 2018 at 9:36 AM Per Bothner <xxxxxx@bothner.com> wrote:
Arthur, could you check this patch in? 

Thank you.  I've applied this patch and pushed it to the Github repository:


Thank you to Per and to Jeremy for reporting the issue.