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

.github/deploy.sh

@@ -8,8 +8,8 @@ rm -rf out/master/ || exit 0
 echo "Making the docs for master"
 mkdir out/master/
 cp util/gh-pages/index.html out/master
+cp util/gh-pages/theme.js out/master
 cp util/gh-pages/script.js out/master
-cp util/gh-pages/lints.json out/master
 cp util/gh-pages/style.css out/master
 
 if [[ -n $TAG_NAME ]]; then