52b8324503
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` |
||
|---|---|---|
| .. | ||
| index_template.html | ||
| script.js | ||
| style.css | ||
| theme.js | ||
| versions.html | ||