Mirrors/rust-clippy
2
0
Fork 0
mirror of https://github.com/rust-lang/rust-clippy synced 2024-11-22 20:53:21 +00:00
Code Issues Projects Releases Packages Wiki Activity
rust-clippy/util
History
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):

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

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 Fix version.py after deleting v* dirs 2023-06-17 10:05:06 +02:00