Auto merge of #13588 - GuillaumeGomez:fix-lint-anchor, r=flip1995

Fix not working lint anchor (generation and filtering)

As spotted by `@flip1995,` the anchor button is currently not working. Problem was the JS that was preventing the web browser from adding the hash at the end of the URL.

For the second bug fixed, the JS was stripping two characters instead of just stripping the `#` at the beginning.

changelog: Fix clippy page lint anchor (generation and filtering)

r? `@flip1995`

2 files changed, 8 insertions, 5 deletions

diff --git a/util/gh-pages/index_template.html b/util/gh-pages/index_template.html
index 012d4806c6c..f95fe76d996 100644
--- a/util/gh-pages/index_template.html
+++ b/util/gh-pages/index_template.html
@@ -150,7 +150,7 @@ Otherwise, have a great day =^.^=
                             <h2 class="panel-title"> {# #}
                                 <div class="panel-title-name" id="lint-{{lint.id}}"> {# #}
                                     <span>{{lint.id}}</span> {#+ #}
-                                    <a href="#{{lint.id}}" class="anchor label label-default" onclick="openLint(event)">&para;</a> {#+ #}
+                                    <a href="#{{lint.id}}" onclick="lintAnchor(event)" class="anchor label label-default">&para;</a> {#+ #}
                                     <a href="" class="anchor label label-default" onclick="copyToClipboard(event)"> {# #}
                                         &#128203; {# #}
                                     </a> {# #}
diff --git a/util/gh-pages/script.js b/util/gh-pages/script.js
index ac928621362..9a5365b2158 100644
--- a/util/gh-pages/script.js
+++ b/util/gh-pages/script.js
@@ -151,11 +151,14 @@ function expandLint(lintId) {
     highlightIfNeeded(lintId);
 }
 
-// Show details for one lint
-function openLint(event) {
+function lintAnchor(event) {
     event.preventDefault();
     event.stopPropagation();
-    expandLint(event.target.getAttribute("href").slice(1));
+
+    const id = event.target.getAttribute("href").replace("#", "");
+    window.location.hash = id;
+
+    expandLint(id);
 }
 
 function copyToClipboard(event) {
@@ -519,7 +522,7 @@ function scrollToLint(lintId) {
 
 // If the page we arrive on has link to a given lint, we scroll to it.
 function scrollToLintByURL() {
-    const lintId = window.location.hash.substring(2);
+    const lintId = window.location.hash.substring(1);
     if (lintId.length > 0) {
         scrollToLint(lintId);
     }