diff --git a/util/gh-pages/index_template.html b/util/gh-pages/index_template.html index 9779e317fd7..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 =^.^=

{# #}
{# #} {{lint.id}} {#+ #} - {#+ #} + {#+ #} {# #} 📋 {# #} {# #} diff --git a/util/gh-pages/script.js b/util/gh-pages/script.js index 9928c86a98f..9a5365b2158 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();