888c34ad70
The rustc's PR wasn't merged. Hopefully this commit can simply be reverted when it's time.
The rustc's PR wasn't merged. Hopefully this commit can simply be reverted when it's time.