bors 646f973857 Auto merge of #14134 - lnicola:clippy-manual, r=Veykril ... feat: Add clippy configuration section to the manual and update some old keys Closes #14132 I don't think this is supposed to be under `Diagnostics`, but it does make sense in a way 🤷 (it's probably where someone might look).		2023-02-12 09:53:15 +00:00
..
dev	Add a 'open server logs' button to the error notification	2023-01-23 13:24:42 +01:00
user	Auto merge of #14134 - lnicola:clippy-manual, r=Veykril	2023-02-12 09:53:15 +00:00