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

Auto merge of #8839 - Serial-ATA:copy-lint-name, r=xFrednet

Browse Source 
Add copy lint name button

changelog: Documentation: Add a *copy lint name*-button to Clippy's lint list

closes #7959
This commit is contained in:
bors 2022-05-18 20:50:54 +00:00
commit 6f8d18fe69
2 changed files with 24 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
util/gh-pages/index.html
View File

@ -490,6 +490,9 @@ Otherwise, have a great day =^.^=
<div class="panel-title-name">
<span>{{lint.id}}</span>
<a href="#{{lint.id}}" class="anchor label label-default" ng-click="open[lint.id] = true; $event.stopPropagation()">&para;</a>
<a href="" id="clipboard-{{lint.id}}" class="anchor label label-default" ng-click="copyToClipboard(lint); $event.stopPropagation()">
&#128203;
</a>
</div>
<div class="panel-title-addons">

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

@ -258,6 +258,27 @@
return true;
}
$scope.copyToClipboard = function (lint) {
const clipboard = document.getElementById("clipboard-" + lint.id);
if (clipboard) {
let resetClipboardTimeout = null;
let resetClipboardIcon = clipboard.innerHTML;
function resetClipboard() {
resetClipboardTimeout = null;
clipboard.innerHTML = resetClipboardIcon;
}
navigator.clipboard.writeText("clippy::" + lint.id);
clipboard.innerHTML = "&#10003;";
if (resetClipboardTimeout !== null) {
clearTimeout(resetClipboardTimeout);
}
resetClipboardTimeout = setTimeout(resetClipboard, 1000);
}
}
// Get data
$scope.open = {};
$scope.loading = true;