From 82969e5c4e074c31cc94678d39d64bacf182a4f6 Mon Sep 17 00:00:00 2001 From: Guillaume Gomez Date: Sat, 12 Oct 2024 00:00:10 +0200 Subject: [PATCH] Allow to go through clippy lints page without javascript --- util/gh-pages/index_template.html | 37 +++++++++++++++++-------------- util/gh-pages/script.js | 11 +++++---- util/gh-pages/style.css | 22 +++++++++++++++--- 3 files changed, 44 insertions(+), 26 deletions(-) diff --git a/util/gh-pages/index_template.html b/util/gh-pages/index_template.html index 663ef1fbd31..c9f99000de5 100644 --- a/util/gh-pages/index_template.html +++ b/util/gh-pages/index_template.html @@ -143,26 +143,29 @@ Otherwise, have a great day =^.^= {# #} {% for lint in lints %} -