mirror of
https://github.com/rust-lang/rust.git
synced 2025-10-27 11:05:06 +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