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

..

index.html

Update URL in rendered docs Github ribbon

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

versions.html

Generate version index for docs domain index

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