I've pushed these as 9e2669690c80dc00973859edf732964f0a514d7b now, so
closing.

Thanks!