diff options
| author | bors <bors@rust-lang.org> | 2024-11-02 13:49:04 +0000 |
|---|---|---|
| committer | bors <bors@rust-lang.org> | 2024-11-02 13:49:04 +0000 |
| commit | 52b8324503d670646bc54a976bbc6baa9ddde08e (patch) | |
| tree | 4ee165b164692ff9ae2a93ec786105ce9913f1bf | |
| parent | 5c6fe68c006b83eeef0f7f0213cf04c7865f7585 (diff) | |
| parent | ac764df8ab342d5d58ec0a51d900949db68f70ad (diff) | |
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`
| -rw-r--r-- | util/gh-pages/index_template.html | 4 | ||||
| -rw-r--r-- | util/gh-pages/style.css | 17 | ||||
| -rw-r--r-- | util/gh-pages/theme.js | 4 |
3 files changed, 22 insertions, 3 deletions
diff --git a/util/gh-pages/index_template.html b/util/gh-pages/index_template.html index f95fe76d996..deb0ef0b499 100644 --- a/util/gh-pages/index_template.html +++ b/util/gh-pages/index_template.html @@ -52,12 +52,12 @@ Otherwise, have a great day =^.^= <noscript> {# #} <div class="alert alert-danger" role="alert"> {# #} - Sorry, this site only works with JavaScript! :( {# #} + Lints search and filtering only works with JS enabled. :( {# #} </div> {# #} </noscript> {# #} <div> {# #} - <div class="panel panel-default"> {# #} + <div class="panel panel-default" id="menu-filters"> {# #} <div class="panel-body row"> {# #} <div id="upper-filters" class="col-12 col-md-5"> {# #} <div class="btn-group" id="lint-levels" tabindex="-1"> {# #} diff --git a/util/gh-pages/style.css b/util/gh-pages/style.css index d207996ab2f..896f2fdac76 100644 --- a/util/gh-pages/style.css +++ b/util/gh-pages/style.css @@ -204,7 +204,7 @@ details[open] { } /* Expanding the mdBook theme*/ -.light { +.light, body:not([class]) { --inline-code-bg: #f6f7f6; } .rust { @@ -220,6 +220,21 @@ details[open] { --inline-code-bg: #191f26; } +@media (prefers-color-scheme: dark) { + body:not([class]) { + /* + In case JS is disabled and the user's system is in dark mode, we take "coal" as default + dark theme. + */ + --inline-code-bg: #1d1f21; + } +} + +html:not(.js) #settings-dropdown, +html:not(.js)#menu-filters { + display: none; +} + #settings-dropdown { position: absolute; margin: 0.7em; diff --git a/util/gh-pages/theme.js b/util/gh-pages/theme.js index bc296955ddf..90f57d4469d 100644 --- a/util/gh-pages/theme.js +++ b/util/gh-pages/theme.js @@ -45,6 +45,10 @@ function setTheme(theme, store) { } (function() { + // This file is loaded first. If so, we add the `js` class on the `<html>` + // element. + document.documentElement.classList.add("js"); + // loading the theme after the initial load const prefersDark = window.matchMedia("(prefers-color-scheme: dark)"); const theme = loadValue("theme"); |
