Improve display of clippy lints page when JS is disabled

GuillaumeGomez · GuillaumeGomez · commit 06de55034f9f · 2024-11-01T20:13:16.000+01:00
diff --git a/util/gh-pages/index_template.html b/util/gh-pages/index_template.html
@@ -24,6 +24,7 @@
     <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 @@ <h1>Clippy Lints</h1> {# #}
 
         <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
@@ -0,0 +1,3 @@
+#settings-dropdown, #menu-filters {
+    display: none;
+}

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+#settings-dropdown, #menu-filters {`
	`2`	`+ display: none;`
	`3`	`+}`