Pascal Hertleif b3c90efcb4 Generate version index for docs domain index ... Uses basically the same code as the lint docs page as I didn't want to reinvent anything: A simple python script (inline in deploy script) writes an array of versions to a JSON file, which gets turned into a list of links using a bit of angular.js code. Fixes #1917		2017-08-03 21:21:59 +02:00
..
deploy.sh	Generate version index for docs domain index	2017-08-03 21:21:59 +02:00
deploy_key.enc	Setup automatic push of gh-pages	2016-07-19 21:26:16 +02:00
ISSUE_TEMPLATE.md	Add a issue template and specify a *recent* nightly is needed	2016-06-10 13:47:47 +02:00