On Mon, 11 Jan 2016 13:22:35 +0100, Pedro Alves wrote:
> OK with that change.

Done, checked in.


Thanks,
Jan