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

1 files changed, 13 insertions, 0 deletions

diff --git a/.github/deploy.sh b/.github/deploy.sh
index 47bf021c626..8f6abc93ecf 100755
--- a/.github/deploy.sh
+++ b/.github/deploy.sh
@@ -33,6 +33,19 @@ if [ -n "$TRAVIS_TAG" ]; then
     ln -s "$TRAVIS_TAG" out/current
 fi
 
+# Generate version index that is shown as root index page
+(
+    cp util/gh-pages/versions.html out/index.html
+
+    cd out
+    python -c '\
+        import os, json;\
+        print json.dumps([\
+            dir for dir in os.listdir(".")\
+            if not dir.startswith(".") and os.path.isdir(dir)\
+        ])' > versions.json
+)
+
 # Pull requests and commits to other branches shouldn't try to deploy, just build to verify
 if [ "$TRAVIS_PULL_REQUEST" != "false" ] || [ "$TRAVIS_BRANCH" != "$SOURCE_BRANCH" ]; then
     # Tags should deploy