Added render tooling.

mdheader.htm

@@ -0,0 +1,4 @@
+<meta name="viewport" content="width=device-width, initial-scale=1.0"/>
+
+<link rel="stylesheet" href="style.css" type="text/css"/>
+<link rel="stylesheet" href="markdown.css" type="text/css"/>

render.py

@@ -0,0 +1,42 @@
+#!/usr/bin/env python3
+
+import os
+import subprocess
+import sys
+import shutil
+import pathlib
+
+output = sys.argv[1]
+
+print('exporting to \'' + output + '\'')
+
+# Make sure the directory doesn't already exist.
+if not os.path.exists(output):
+    os.mkdir(output)
+else:
+    print('directory already exists!')
+    sys.exit(1)
+
+# Copy the static files
+for dp, dns, fns in os.walk('static'):
+    for fn in fns:
+        if fn.endswith('~'):
+            continue
+        shutil.copy2(os.path.join(dp, fn), os.path.join(output, fn))
+
+# Convert and export the markdown files.
+def export_markdown(f):
+    outfile = os.path.splitext(os.path.join(output, f))[0] + '.html'
+    try:
+        os.makedirs(os.path.dirname(outfile))
+    except:
+        pass
+    cmd = 'pandoc --from gfm --to html --standalone --include-in-header=mdheader.htm -o ' + outfile + ' markdown/' + f
+    subprocess.run(cmd.split(), shell=False)
+
+for dp, dns, fns in os.walk('markdown'):
+    for fn in fns:
+        if fn.endswith('~'):
+            continue
+        export_markdown(os.path.relpath(os.path.join(dp, fn), 'markdown'))
+

static/style.css

@@ -0,0 +1,43 @@
+/* CSS for tr3y.io */
+
+body {
+    font-family: sans-serif;
+    max-width: 42em;
+}
+
+a.button {
+    margin: 5px;
+    border: 1px solid #999;
+    border-radius: 2px;
+    padding: 4px;
+    background-color: #bbb;
+    text-decoration: none;
+    color: #000;
+}
+
+a.button:link, a.button:visited, a.button:hover, a.button:active {
+    color: #000;
+}
+
+h1 {
+    border-bottom: 2px solid black;
+}
+
+h2 {
+    border-bottom: 1px solid #999;
+}
+
+h3 {
+    border-bottom: 1px solid #aaa;
+}
+
+h4 {
+    border-bottom: 1px dotted #aaa;
+}
+
+img.iconthumb {
+    margin: 0.5em;
+    border: 2px solid #222;
+    border-radius: 0.5em;
+    width: 30%;
+}