bors 8ae74da63b Auto merge of #8070 - CrazyRoka:update-gh-pages-checkbox-styles, r=camsteffen ...

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

2022-03-10 03:08:34 +00:00

..

etc

Add includes to pre-commit hook

2021-09-29 05:46:43 +02:00

gh-pages

Auto merge of #8070 - CrazyRoka:update-gh-pages-checkbox-styles, r=camsteffen

2022-03-10 03:08:34 +00:00

fetch_prs_between.sh

…

versions.py

Remove old python lint doc generation scripts

2021-07-28 14:18:40 +02:00