@cmr Yeah, that's a good point. I'll add this after https://github.com/mozilla/rust/pull/14009 lands.