Added copy lint name button to lint list

Fixes rust-lang#7959
Mastermindaxe · Feb 25, 2022 · a7fc3a3 · a7fc3a3
1 parent 7b2896a
commit a7fc3a3
Showing 1 changed file with 6 additions and 0 deletions.
diff --git 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;