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:  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
gh-pages	Auto merge of #13585 - GuillaumeGomez:no-js, r=Alexendoo	2024-11-02 13:49:04 +00:00
fetch_prs_between.sh
versions.py	Remove unused import from Clippy versions.py file	2024-09-24 18:13:17 +02:00