about summary refs log tree commit diff
diff options
context:
space:
mode:
authorSamuel Tardieu <sam@rfc1149.net>2025-05-30 08:07:49 +0000
committerGitHub <noreply@github.com>2025-05-30 08:07:49 +0000
commit77f4e0021904a09f7900cb1957eeeb541e03931a (patch)
tree47a33c86e67803e31b1e042c7b3e8c5fee750c06
parent6275f5235a939832b972e3d32c9fbff107f0bb34 (diff)
parent8cced0fd6fd9c2b434ac08c09c160b026ed6b691 (diff)
downloadrust-77f4e0021904a09f7900cb1957eeeb541e03931a.tar.gz
rust-77f4e0021904a09f7900cb1957eeeb541e03931a.zip
Show total count lints (#14901)
Suppose it might be interesting to see up to date total number of lints
something like this

<img width="1276" alt="Screenshot 2025-05-26 at 21 35 46"
src="https://github.com/user-attachments/assets/66c67eb4-f4c6-44ae-9bf4-284a4c4da3e0"
/>
changelog: none
-rw-r--r--util/gh-pages/index_template.html2
-rw-r--r--util/gh-pages/script.js12
2 files changed, 13 insertions, 1 deletions
diff --git a/util/gh-pages/index_template.html b/util/gh-pages/index_template.html
index 19dc1ec0b0c..865b9523c39 100644
--- a/util/gh-pages/index_template.html
+++ b/util/gh-pages/index_template.html
@@ -50,7 +50,7 @@ Otherwise, have a great day =^.^=
 
     <div class="container"> {# #}
         <div class="page-header"> {# #}
-            <h1>Clippy Lints</h1> {# #}
+            <h1>Clippy Lints <span id="lint-count" class="badge"></span></h1> {# #}
         </div> {# #}
 
         <noscript> {# #}
diff --git a/util/gh-pages/script.js b/util/gh-pages/script.js
index c942a6a05a1..fec883938d6 100644
--- a/util/gh-pages/script.js
+++ b/util/gh-pages/script.js
@@ -71,6 +71,7 @@ window.searchState = {
         } else {
             window.location.hash = '';
         }
+        updateLintCount();
     },
 };
 
@@ -598,3 +599,14 @@ generateSearch();
 parseURLFilters();
 scrollToLintByURL();
 filters.filterLints();
+updateLintCount();
+
+function updateLintCount() {
+    const allLints = filters.getAllLints();
+    const totalLints = allLints.length;
+    
+    const countElement = document.getElementById("lint-count");
+    if (countElement) {
+        countElement.innerText = `Total number: ${totalLints}`;
+    }
+}