diff --git a/util/gh-pages/index.html b/util/gh-pages/index.html
index 1171da3f4e5..2076d129978 100644
--- a/util/gh-pages/index.html
+++ b/util/gh-pages/index.html
@@ -490,6 +490,9 @@ Otherwise, have a great day =^.^=
diff --git a/util/gh-pages/script.js b/util/gh-pages/script.js
index c3250afdea2..bf4ce79b2cb 100644
--- a/util/gh-pages/script.js
+++ b/util/gh-pages/script.js
@@ -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 = "✓";
+ if (resetClipboardTimeout !== null) {
+ clearTimeout(resetClipboardTimeout);
+ }
+ resetClipboardTimeout = setTimeout(resetClipboard, 1000);
+ }
+ }
+
// Get data
$scope.open = {};
$scope.loading = true;