Add copy lint name button

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">

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;