<div dir="ltr"><div class="gmail_extra">Ahh yes, of course -- John has done it, and it's been merged here: ddfaef6bb28e697491b25bff5a7b260d44ce6ccf
</div></div>