Auto merge of rust-lang#13187 - GuillaumeGomez:settings-menu, r=Alexendoo

Add settings menu on clippy lints page

It looks like this (when the menu is expanded):

![Screenshot from 2024-08-06 21-36-41](https://github.com/user-attachments/assets/c464aef3-b21e-48cc-8e3a-c32a134f995e)

Follow-up of rust-lang/rust-clippy#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

Author: bors

.github/deploy.sh

@@ -10,6 +10,7 @@ mkdir out/master/
 cp util/gh-pages/index.html out/master
 cp util/gh-pages/script.js out/master
 cp util/gh-pages/lints.json out/master
+cp util/gh-pages/style.css out/master
 
 if [[ -n $TAG_NAME ]]; then
   echo "Save the doc for the current tag ($TAG_NAME) and point stable/ to it"