Skip to content

Commit

Permalink
Auto merge of #13588 - GuillaumeGomez:fix-lint-anchor, r=flip1995
Browse files Browse the repository at this point in the history
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`
  • Loading branch information
bors committed Oct 23, 2024
2 parents 5873cb9 + 7115404 commit cefa31a
Show file tree
Hide file tree
Showing 2 changed files with 8 additions and 5 deletions.
2 changes: 1 addition & 1 deletion util/gh-pages/index_template.html
Original file line number Diff line number Diff line change
Expand Up @@ -150,7 +150,7 @@ <h1>Clippy Lints</h1> {# #}
<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> {# #}
Expand Down
11 changes: 7 additions & 4 deletions util/gh-pages/script.js
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down Expand Up @@ -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);
}
Expand Down

0 comments on commit cefa31a

Please sign in to comment.