mirror of
https://github.com/rust-lang/rust.git
synced 2025-10-15 16:58:02 +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