diff options
Diffstat (limited to 'src/tools/clippy/util/gh-pages/script.js')
| -rw-r--r-- | src/tools/clippy/util/gh-pages/script.js | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/tools/clippy/util/gh-pages/script.js b/src/tools/clippy/util/gh-pages/script.js index fec883938d6..285aa34e701 100644 --- a/src/tools/clippy/util/gh-pages/script.js +++ b/src/tools/clippy/util/gh-pages/script.js @@ -602,7 +602,7 @@ filters.filterLints(); updateLintCount(); function updateLintCount() { - const allLints = filters.getAllLints(); + const allLints = filters.getAllLints().filter(lint => lint.group != "deprecated"); const totalLints = allLints.length; const countElement = document.getElementById("lint-count"); |