diff options
| author | Guillaume Gomez <guillaume1.gomez@gmail.com> | 2024-10-22 18:33:55 +0200 |
|---|---|---|
| committer | Guillaume Gomez <guillaume1.gomez@gmail.com> | 2024-11-01 20:20:12 +0100 |
| commit | c056928af2fb09dd667c6c037bc09b0f25e7e2e3 (patch) | |
| tree | 3e9dd3a1272db1dd4591bb1ffa51bd9b3a9963f5 | |
| parent | 5873cb9d1752946f1f0a41512b45697879245ca0 (diff) | |
| download | rust-c056928af2fb09dd667c6c037bc09b0f25e7e2e3.tar.gz rust-c056928af2fb09dd667c6c037bc09b0f25e7e2e3.zip | |
Improve display of clippy lints page when JS is disabled
| -rw-r--r-- | util/gh-pages/index_template.html | 5 | ||||
| -rw-r--r-- | util/gh-pages/noscript.css | 3 |
2 files changed, 6 insertions, 2 deletions
diff --git a/util/gh-pages/index_template.html b/util/gh-pages/index_template.html index 012d4806c6c..061777809b9 100644 --- a/util/gh-pages/index_template.html +++ b/util/gh-pages/index_template.html @@ -24,6 +24,7 @@ Otherwise, have a great day =^.^= <link id="styleNight" rel="stylesheet" href="https://rust-lang.github.io/mdBook/tomorrow-night.css" disabled="true"> {# #} <link id="styleAyu" rel="stylesheet" href="https://rust-lang.github.io/mdBook/ayu-highlight.css" disabled="true"> {# #} <link rel="stylesheet" href="style.css"> {# #} + <noscript><link rel="stylesheet" href="noscript.css"></noscript> {# #} </head> {# #} <body> {# #} <script src="theme.js"></script> {# #} @@ -52,12 +53,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/noscript.css b/util/gh-pages/noscript.css new file mode 100644 index 00000000000..907509ce314 --- /dev/null +++ b/util/gh-pages/noscript.css @@ -0,0 +1,3 @@ +#settings-dropdown, #menu-filters { + display: none; +} |