On Thu, 14 Dec 2017 00:03:12 +0100, Pedro Alves wrote:
> OK with those fixed.

Checked in.


Thanks,
Jan