On 04/10/2018 21:39, Richard Sandiford wrote:
> OK with that change if it works, thanks.

Thanks, here's what I've committed.

Andrew