8ae74da63b
Improve styles of filtering options for Clippy's lint list Partially solves #7958 Updated styles for filtering options. It now uses dropdown menus. ![image](https://user-images.githubusercontent.com/19844144/144608479-cdd9de0b-f101-4d49-a135-0969efb01a11.png) changelog: none |
||
---|---|---|
.. | ||
etc | ||
gh-pages | ||
fetch_prs_between.sh | ||
versions.py |