Matthias Krüger 68f12338af Rollup merge of #104505 - WaffleLapkin:no-double-spaces-in-comments, r=jackh726 ... Remove double spaces after dots in comments Most of the comments do not have double spaces, so I assume these are typos.		2023-01-17 20:21:25 +01:00
..
map	Remove double spaces after dots in comments	2023-01-17 08:09:33 +00:00
mod.rs	Rollup merge of #104505 - WaffleLapkin:no-double-spaces-in-comments, r=jackh726	2023-01-17 20:21:25 +01:00
nested_filter.rs	Reword comments and rename HIR visiting methods.	2022-07-07 16:01:43 +02:00
place.rs	Add #[derive(TypeVisitable)]	2022-07-05 22:25:15 +01:00