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

Reply via email to