diff options
| -rw-r--r-- | util/gh-pages/index_template.html | 2 | ||||
| -rw-r--r-- | util/gh-pages/script.js | 11 |
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)">¶</a> {#+ #} + <a href="#{{lint.id}}" onclick="lintAnchor(event)" class="anchor label label-default">¶</a> {#+ #} <a href="" class="anchor label label-default" onclick="copyToClipboard(event)"> {# #} 📋 {# #} </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); } |