docs: add an extension to generate redirects

Reviewed-by: Eric Engestrom <eric@engestrom.ch> Part-of: <https://gitlab.freedesktop.org/mesa/mesa/-/merge_requests/5706>
2020-07-02 12:14:28 +02:00
parent ce5a3524fa
commit 64a4ba9e1c
2 changed files with 20 additions and 1 deletions
--- a/docs/_exts/redirects.py
+++ b/docs/_exts/redirects.py
@@ -0,0 +1,19 @@
+import os
+
+redirects = []
+
+def create_redirect(dst):
+    tpl = '<html><head><meta http-equiv="refresh" content="0; url={0}"><script>window.location.replace("{0}")</script></head></html>'
+    return tpl.format(dst)
+
+def create_redirects(app, docname):
+    if not app.builder.name == 'html':
+        return
+    for src, dst in redirects:
+        path = os.path.join(app.outdir, '{0}.html'.format(src))
+        url = '{0}.html'.format(dst)
+        with open(path, 'w') as f:
+            f.write(create_redirect(url))
+
+def setup(app):
+    app.connect('build-finished', create_redirects)