bors c7c8724897 Auto merge of #13187 - GuillaumeGomez:settings-menu, r=Alexendoo ... Add settings menu on clippy lints page It looks like this (when the menu is expanded):  Follow-up of https://github.com/rust-lang/rust-clippy/pull/13178. Someone pointed out that they should be able to disable the shortcuts on this page like it's the case for rustdoc and docs.rs. So here we go. The first commit moves the style into its own file: it's much better for a web browser because it can then cache it. The second one actually adds the new settings menu you can see above. r? `@Alexendoo` changelog: Add settings menu on clippy lints page		2024-08-11 18:42:37 +00:00
..
etc	Port clippy away from compiletest to ui_test	2023-06-26 14:13:07 +00:00
gh-pages	Auto merge of #13187 - GuillaumeGomez:settings-menu, r=Alexendoo	2024-08-11 18:42:37 +00:00
fetch_prs_between.sh	Fix changelog PR listings, create them automatically in fetch_prs_between.sh	2023-07-07 12:07:05 +00:00
versions.py