On 2017-05-05 14:04, Ken Brown wrote: > The attached patch fixes an annoyance similar to the one fixed by commit > d5ac4d52411459192ee59a98cf1344f6eac17f33. Merged. Thanks, -- Yaakov