Closed
Description
I often want to copy the lint name when searching for something on Clippy's lint list. It would be helpful to have a "copy lint name"-button next to the name, similar to the "link"-button that currently exist.
The current "link"-button looks like this:
The HTML document of the page can be found under util/gh-pages/index.html
. cargo dev serve
can be used to test the changes locally.
Main tracking issue #7172