From a7fc3a3313996a0fef44744131b04d4ac7d0d9b9 Mon Sep 17 00:00:00 2001
From: Florian Nagel <florian.nagel@senacor.com>
Date: Fri, 25 Feb 2022 16:26:11 +0100
Subject: [PATCH] Added copy lint name button to lint list

Fixes #7959
---
 util/gh-pages/index.html | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/util/gh-pages/index.html b/util/gh-pages/index.html
index 83a200ca3c4f..87749c7257ff 100644
--- a/util/gh-pages/index.html
+++ b/util/gh-pages/index.html
@@ -322,6 +322,7 @@ <h2 class="panel-title">
                         <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="" class="anchor label label-default" title="Copy to clipboard" ng-click="copyToClipboard(lint); $event.stopPropagation()">&#128203;</a>
                         </div>
 
                         <div class="panel-title-addons">
@@ -499,6 +500,11 @@ <h2 class="panel-title">
                 return true;
             }
 
+            $scope.copyToClipboard = function (lint) {
+                navigator.clipboard.writeText(lint.id);
+                alert('Copied `' + lint.id + '` to clipboard!');
+            }
+
             // Get data
             $scope.open = {};
             $scope.loading = true;