![]() Improve styles of filtering options for Clippy's lint list Partially solves #7958 Updated styles for filtering options. It now uses dropdown menus.  changelog: none |
||
---|---|---|
.. | ||
etc | ||
gh-pages | ||
fetch_prs_between.sh | ||
versions.py |