diff options
| -rw-r--r-- | util/gh-pages/index_template.html | 2 | ||||
| -rw-r--r-- | util/gh-pages/script.js | 12 |
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}`; + } +} |
