bors 6f1def79dd Auto merge of #13269 - GuillaumeGomez:rewrite-lints-page, r=Alexendoo ... Rewrite lints page This PR has multiple goals: * Make lints page to work without needing a web server by removing the json file. * Prepare the field to also make the page work with JS (not done in this PR but should be straightforward). * Remove angular dependency. r? `@Alexendoo` changelog: make lint page work without web server		2024-10-11 14:18:54 +00:00
..
etc	Merge commit '37f4c1725d3fd7e9c3ffd8783246bc5589debc53' into clippyup	2023-07-02 14:59:02 +02:00
gh-pages	Greatly reduce generated HTML page size	2024-10-03 11:17:33 +02:00
fetch_prs_between.sh	Merge commit 'd9c24d1b1ee61f276e550b967409c9f155eac4e3' into clippyup	2023-07-17 10:22:32 +02:00
versions.py	Remove unused import from Clippy versions.py file	2024-09-24 18:13:17 +02:00