From b3c90efcb43a19d4c65eb7cbd4f406ede7b2a7f3 Mon Sep 17 00:00:00 2001
From: Pascal Hertleif <killercup@gmail.com>
Date: Thu, 3 Aug 2017 21:17:12 +0200
Subject: 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
---
 .github/deploy.sh | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to '.github/deploy.sh')

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
-- 
cgit 1.4.1-3-g733a5