Added copy lint name button to lint list

Fixes rust-lang#7959

Author: florian-nagel

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;