From 0fd03a85deb7f423f4b0f869b1e9ea20bb9b748e Mon Sep 17 00:00:00 2001
From: Serial <69764315+Serial-ATA@users.noreply.github.com>
Date: Sun, 22 May 2022 15:24:47 -0400
Subject: [PATCH] Strip `clippy::` prefix from search strings

---
 util/gh-pages/script.js | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/util/gh-pages/script.js b/util/gh-pages/script.js
index 68e65acf9cb..6909fbcae09 100644
--- 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) {