1 files changed, 33 insertions, 0 deletions
diff --git a/admin/serve-doc b/admin/serve-doc
new file mode 100755
index 000000000..fa2805938
--- /dev/null
+++ b/admin/serve-doc
@@ -0,0 +1,33 @@
+#!/usr/bin/python3
+
+from __future__ import print_function
+
+import http.server
+import socketserver
+import os
+import sys
+
+path = os.path.dirname(sys.argv[0])
+os.chdir(path)
+os.chdir('..')
+os.chdir('build-doc/output/html')
+
+class ReusingTCPServer(http.server.SimpleHTTPRequestHandler):
+    allow_reuse_address = True
+
+    def send_head(self):
+        # horrible kludge because SimpleHTTPServer is buggy wrt
+        # slash-redirecting of requests with query arguments, and will
+        # redirect to /foo?q=bar/ -- wrong slash placement
+        self.path = self.path.split('?', 1)[0]
+        return http.server.SimpleHTTPRequestHandler.send_head(self)
+
+httpd = socketserver.TCPServer(
+    ("", 8080),
+    ReusingTCPServer,
+    )
+try:
+    print("Serving doc at port: http://localhost:8080")
+    httpd.serve_forever()
+except KeyboardInterrupt:
+    pass