From c056928af2fb09dd667c6c037bc09b0f25e7e2e3 Mon Sep 17 00:00:00 2001 From: Guillaume Gomez Date: Tue, 22 Oct 2024 18:33:55 +0200 Subject: [PATCH] Improve display of clippy lints page when JS is disabled --- util/gh-pages/index_template.html | 5 +++-- util/gh-pages/noscript.css | 3 +++ 2 files changed, 6 insertions(+), 2 deletions(-) create mode 100644 util/gh-pages/noscript.css 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 =^.^= {# #} {# #} {# #} + {# #} {# #} {# #} {# #} @@ -52,12 +53,12 @@ Otherwise, have a great day =^.^= {# #}
{# #} -
{# #} +