Strip clippy:: prefix from search strings

2022-05-22 15:24:47 -04:00 · 2022-05-22 15:24:47 -04:00 · 0fd03a85de
commit 0fd03a85de
parent 91644d1f1d
1 changed files with 3 additions and 0 deletions
--- a/util/gh-pages/script.js
+++ b/util/gh-pages/script.js
@ -232,6 +232,9 @@
                    return true;
                }
                searchStr = searchStr.toLowerCase();
+                if (searchStr.startsWith("clippy::")) {
+                    searchStr = searchStr.slice(8);
+                }

                // Search by id
                if (lint.id.indexOf(searchStr.replace("-", "_")) !== -1) {