From ecb397a3650d9a6001a2c3a7b51f395c1625727a Mon Sep 17 00:00:00 2001 From: Guillaume Gomez Date: Wed, 25 Jun 2025 20:39:14 +0200 Subject: [PATCH] Reduce page size and number of DOM elements on clippy lints page --- util/gh-pages/index_template.html | 28 ++++++++++++---------------- util/gh-pages/style.css | 19 +++++++++++++++++-- 2 files changed, 29 insertions(+), 18 deletions(-) diff --git a/util/gh-pages/index_template.html b/util/gh-pages/index_template.html index 865b9523c39e..458f20d9f99c 100644 --- a/util/gh-pages/index_template.html +++ b/util/gh-pages/index_template.html @@ -149,25 +149,21 @@

Clippy Lints

{# #}
{# #} {# #} {# #}
{# #} diff --git a/util/gh-pages/style.css b/util/gh-pages/style.css index 3cc7a919c23a..046a2a5df7c4 100644 --- a/util/gh-pages/style.css +++ b/util/gh-pages/style.css @@ -50,8 +50,23 @@ div.panel div.panel-body button.open { .panel-heading { cursor: pointer; } -.panel-title { display: flex; flex-wrap: wrap;} -.panel-title .label { display: inline-block; } +.lint-title { + cursor: pointer; + margin-top: 0; + margin-bottom: 0; + font-size: 16px; + display: flex; + flex-wrap: wrap; + background: var(--theme-hover); + color: var(--fg); + border: 1px solid var(--theme-popup-border); + padding: 10px 15px; + border-top-left-radius: 3px; + border-top-right-radius: 3px; + gap: 4px; +} + +.lint-title .label { display: inline-block; } .panel-title-name { flex: 1; min-width: 400px;} .panel-title-name span { vertical-align: bottom; }