On 15-07-31 01:18 PM, Pedro Alves wrote: > Many thanks for doing this! > > At least two people looked over this issues now, and I read it all > again now, and it still all looks obviously correct. Thus, > > OK. Well, that was quick! Pushed, thanks.