mikros/rust
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Improve display of clippy lints page when JS is disabled

Browse Source
This commit is contained in:
Guillaume Gomez 2024-10-22 18:33:55 +02:00
parent 5873cb9d17
commit c056928af2
2 changed files with 6 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
util/gh-pages/index_template.html
View File

@ -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"> {# #}

3
util/gh-pages/noscript.css Normal file
View File

@ -0,0 +1,3 @@
#settings-dropdown, #menu-filters {
display: none;
}