mikros/rust
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Open lint when clicking on its anchor

Browse Source
This commit is contained in:
Guillaume Gomez 2024-10-23 16:58:06 +02:00
parent b33977b852
commit 7115404a97
2 changed files with 11 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
util/gh-pages/index_template.html
View File

@ -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">&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> {# #}

10
util/gh-pages/script.js
View File

@ -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();