It’s been quite a few days, so I’ve just pushed this as 9dc08c9.