diff options
| -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; +} |