Mirrors/rust-clippy
2
0
Fork 0
mirror of https://github.com/rust-lang/rust-clippy synced 2024-11-25 14:10:32 +00:00
Code Issues Projects Releases Packages Wiki Activity
rust-clippy/util
History
bors 52b8324503 Auto merge of #13585 - GuillaumeGomez:no-js, r=Alexendoo 
Improve display of clippy lints page when JS is disabled

There is no point in displaying the settings menu and the filters if JS is disabled. So in this case, this PR simply hides it:

![image](https://github.com/user-attachments/assets/e96039a9-e698-49b7-bf2b-70e78442b305)

For the theme handling though, I need to send a fix to mdBook first. But once done, it'll look as expected (dark if system is in dark mode).

changelog: Improve clippy lints page display when JS is disabled.

r? `@Alexendoo`
2024-11-02 13:49:04 +00:00
..
etc Merge commit '37f4c1725d3fd7e9c3ffd8783246bc5589debc53' into clippyup 2023-07-02 14:59:02 +02:00
gh-pages Auto merge of #13585 - GuillaumeGomez:no-js, r=Alexendoo 2024-11-02 13:49:04 +00:00
fetch_prs_between.sh Merge commit 'd9c24d1b1ee61f276e550b967409c9f155eac4e3' into clippyup 2023-07-17 10:22:32 +02:00
versions.py Remove unused import from Clippy versions.py file 2024-09-24 18:13:17 +02:00