mirror of
https://github.com/rust-lang/rust.git
synced 2025-10-24 05:59:39 +00:00
Revert accidental comment deletion This reverts an accidental comment deletion made in #113128 See also https://github.com/rust-lang/rust/pull/113128#discussion_r1674614882