Closed ghost closed 10 years ago
The new name has been available for a while, and the old one deprecated (though the deprecation warning apparently didn’t work?). It was removed in rust-lang/rust@9d5d97b55d6487ee23b805bc1acbaa0669b82116.
@jdeseno @SimonSapin Thank you. I haven't seen the deprecation warning, and indeed Rust had an issue about that (rust-lang/rust#15702).
This fixes compilation on the latest rust. Just tried this on the nightly so hopefully it isn't premature.