On Mon, 11 Jan 2016 14:38:14 +0100, Pedro Alves wrote:
> OK with that change.

Checked in.


Thanks,
Jan