diff options
| author | Samuel Tardieu <sam@rfc1149.net> | 2025-07-04 10:09:34 +0000 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2025-07-04 10:09:34 +0000 |
| commit | da2f0ad53cb9478993b249bab599ea4b0a52f416 (patch) | |
| tree | cb205b58fb3acfddc232acf08e3181c658d9d054 | |
| parent | 876e05d307c4d39f5a6ba3c61bb19683e6483fac (diff) | |
| parent | ecb397a3650d9a6001a2c3a7b51f395c1625727a (diff) | |
| download | rust-da2f0ad53cb9478993b249bab599ea4b0a52f416.tar.gz rust-da2f0ad53cb9478993b249bab599ea4b0a52f416.zip | |
Reduce page size and number of DOM elements on clippy lints page (#15140)
This is the first pass of "reducing the size of the clippy lints page" I'm currently going through. This first one reduces the size page but mostly reduces the number of DOM elements. Page size change: * Before this PR: 1938957 * With this PR: 1876167 * Reduction: -3.2% r? @Alexendoo changelog: Reduce page size and number of DOM elements on clippy lints page
| -rw-r--r-- | util/gh-pages/index_template.html | 28 | ||||
| -rw-r--r-- | 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 865b9523c39..458f20d9f99 100644 --- a/util/gh-pages/index_template.html +++ b/util/gh-pages/index_template.html @@ -149,25 +149,21 @@ Otherwise, have a great day =^.^= <article class="panel panel-default" id="{{lint.id}}"> {# #} <input id="label-{{lint.id}}" type="checkbox"> {# #} <label for="label-{{lint.id}}"> {# #} - <header class="panel-heading"> {# #} - <h2 class="panel-title"> {# #} - <div class="panel-title-name" id="lint-{{lint.id}}"> {# #} - <span>{{lint.id}}</span> {#+ #} - <a href="#{{lint.id}}" class="lint-anchor anchor label label-default">¶</a> {#+ #} - <a href="" class="copy-to-clipboard anchor label label-default"> {# #} - 📋 {# #} - </a> {# #} - </div> {# #} + <h2 class="lint-title"> {# #} + <div class="panel-title-name" id="lint-{{lint.id}}"> {# #} + <span>{{lint.id}}</span> {#+ #} + <a href="#{{lint.id}}" class="lint-anchor anchor label label-default">¶</a> {#+ #} + <a href="" class="copy-to-clipboard anchor label label-default"> {# #} + 📋 {# #} + </a> {# #} + </div> {# #} - <div class="panel-title-addons"> {# #} - <span class="label label-lint-group label-default label-group-{{lint.group}}">{{lint.group}}</span> {#+ #} + <span class="label label-lint-group label-default label-group-{{lint.group}}">{{lint.group}}</span> {#+ #} - <span class="label label-lint-level label-lint-level-{{lint.level}}">{{lint.level}}</span> {#+ #} + <span class="label label-lint-level label-lint-level-{{lint.level}}">{{lint.level}}</span> {#+ #} - <span class="label label-doc-folding"></span> {# #} - </div> {# #} - </h2> {# #} - </header> {# #} + <span class="label label-doc-folding"></span> {# #} + </h2> {# #} </label> {# #} <div class="list-group lint-docs"> {# #} diff --git a/util/gh-pages/style.css b/util/gh-pages/style.css index 3cc7a919c23..046a2a5df7c 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; } |