From 27fec01fa8268f3fa8cdd0f6b89637e909b2adec Mon Sep 17 00:00:00 2001
From: Serial <69764315+Serial-ATA@users.noreply.github.com>
Date: Wed, 18 May 2022 10:19:50 -0400
Subject: [PATCH 1/3] Add copy lint name button

---
 util/gh-pages/index.html |  3 +++
 util/gh-pages/script.js  | 21 +++++++++++++++++++++
 2 files changed, 24 insertions(+)

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 =^.^=
                         <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">
diff --git a/util/gh-pages/script.js b/util/gh-pages/script.js
index c3250afdea2..b095f6ef16c 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.textContent = "✓";
+                    if (resetClipboardTimeout !== null) {
+                        clearTimeout(resetClipboardTimeout);
+                    }
+                    resetClipboardTimeout = setTimeout(resetClipboard, 1000);
+                }
+            }
+
             // Get data
             $scope.open = {};
             $scope.loading = true;

From 8aae26b227cc77dd713f8b8106324d4d626b75ac Mon Sep 17 00:00:00 2001
From: Serial <69764315+Serial-ATA@users.noreply.github.com>
Date: Wed, 18 May 2022 15:01:02 -0400
Subject: [PATCH 2/3] `innerHTML` -> `textContent`

---
 util/gh-pages/script.js | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/util/gh-pages/script.js b/util/gh-pages/script.js
index b095f6ef16c..4bff225983d 100644
--- a/util/gh-pages/script.js
+++ b/util/gh-pages/script.js
@@ -262,11 +262,11 @@
                 const clipboard = document.getElementById("clipboard-" + lint.id);
                 if (clipboard) {
                     let resetClipboardTimeout = null;
-                    let resetClipboardIcon = clipboard.innerHTML;
+                    let resetClipboardIcon = clipboard.textContent;
 
                     function resetClipboard() {
                         resetClipboardTimeout = null;
-                        clipboard.innerHTML = resetClipboardIcon;
+                        clipboard.textContent = resetClipboardIcon;
                     }
 
                     navigator.clipboard.writeText("clippy::" + lint.id);

From e05da56d6b21dc65367425f1751eaaf2522a9de9 Mon Sep 17 00:00:00 2001
From: Serial <69764315+Serial-ATA@users.noreply.github.com>
Date: Wed, 18 May 2022 15:37:05 -0400
Subject: [PATCH 3/3] `textContent` -> `innerHTML`

---
 util/gh-pages/script.js | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/util/gh-pages/script.js b/util/gh-pages/script.js
index 4bff225983d..bf4ce79b2cb 100644
--- a/util/gh-pages/script.js
+++ b/util/gh-pages/script.js
@@ -262,16 +262,16 @@
                 const clipboard = document.getElementById("clipboard-" + lint.id);
                 if (clipboard) {
                     let resetClipboardTimeout = null;
-                    let resetClipboardIcon = clipboard.textContent;
+                    let resetClipboardIcon = clipboard.innerHTML;
 
                     function resetClipboard() {
                         resetClipboardTimeout = null;
-                        clipboard.textContent = resetClipboardIcon;
+                        clipboard.innerHTML = resetClipboardIcon;
                     }
 
                     navigator.clipboard.writeText("clippy::" + lint.id);
 
-                    clipboard.textContent = "✓";
+                    clipboard.innerHTML = "&#10003;";
                     if (resetClipboardTimeout !== null) {
                         clearTimeout(resetClipboardTimeout);
                     }