From 97d13a8c0a338b2a1d09482cfab463c3b431ae4a Mon Sep 17 00:00:00 2001 From: Guillaume Gomez Date: Tue, 22 Oct 2024 22:50:17 +0200 Subject: [PATCH 1/3] Fix not working lint anchor --- util/gh-pages/index_template.html | 2 +- util/gh-pages/script.js | 7 ------- 2 files changed, 1 insertion(+), 8 deletions(-) diff --git a/util/gh-pages/index_template.html b/util/gh-pages/index_template.html index 012d4806c6cc..9779e317fd79 100644 --- a/util/gh-pages/index_template.html +++ b/util/gh-pages/index_template.html @@ -150,7 +150,7 @@

Clippy Lints

{# #}

{# #}
{# #} {{lint.id}} {#+ #} - {#+ #} + {#+ #} {# #} 📋 {# #} {# #} diff --git a/util/gh-pages/script.js b/util/gh-pages/script.js index ac928621362a..111555ca95fa 100644 --- a/util/gh-pages/script.js +++ b/util/gh-pages/script.js @@ -151,13 +151,6 @@ function expandLint(lintId) { highlightIfNeeded(lintId); } -// Show details for one lint -function openLint(event) { - event.preventDefault(); - event.stopPropagation(); - expandLint(event.target.getAttribute("href").slice(1)); -} - function copyToClipboard(event) { event.preventDefault(); event.stopPropagation(); From b33977b8520bfcf476a30ace4ac2f354e391aeed Mon Sep 17 00:00:00 2001 From: Guillaume Gomez Date: Tue, 22 Oct 2024 22:54:29 +0200 Subject: [PATCH 2/3] Fix invalid lint ID filtering --- util/gh-pages/script.js | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/util/gh-pages/script.js b/util/gh-pages/script.js index 111555ca95fa..9928c86a98f8 100644 --- a/util/gh-pages/script.js +++ b/util/gh-pages/script.js @@ -512,7 +512,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); } From 7115404a975b82dc193fe0b19108d774e1320f37 Mon Sep 17 00:00:00 2001 From: Guillaume Gomez Date: Wed, 23 Oct 2024 16:58:06 +0200 Subject: [PATCH 3/3] Open lint when clicking on its anchor --- util/gh-pages/index_template.html | 2 +- util/gh-pages/script.js | 10 ++++++++++ 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/util/gh-pages/index_template.html b/util/gh-pages/index_template.html index 9779e317fd79..f95fe76d996a 100644 --- a/util/gh-pages/index_template.html +++ b/util/gh-pages/index_template.html @@ -150,7 +150,7 @@

Clippy Lints

{# #}

{# #}
{# #} {{lint.id}} {#+ #} - {#+ #} + {#+ #} {# #} 📋 {# #} {# #} diff --git a/util/gh-pages/script.js b/util/gh-pages/script.js index 9928c86a98f8..9a5365b2158b 100644 --- a/util/gh-pages/script.js +++ b/util/gh-pages/script.js @@ -151,6 +151,16 @@ function expandLint(lintId) { highlightIfNeeded(lintId); } +function lintAnchor(event) { + event.preventDefault(); + event.stopPropagation(); + + const id = event.target.getAttribute("href").replace("#", ""); + window.location.hash = id; + + expandLint(id); +} + function copyToClipboard(event) { event.preventDefault(); event.stopPropagation();