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_key.enc

Setup automatic push of gh-pages

2016-07-19 21:26:16 +02:00

deploy.sh

Generate version index for docs domain index

2017-08-03 21:21:59 +02:00

ISSUE_TEMPLATE.md

Add a issue template and specify a *recent* nightly is needed

2016-06-10 13:47:47 +02:00