updates 33.2 112

ctrl/docs.sh

@@ -0,0 +1,47 @@
+#!/usr/bin/env bash
+# Documentation: serve the pages, and re-render the diagrams.
+#
+# Usage: docs.sh serve [port] | graphs [theme]
+#
+# The docs are a static SPA — index.html plus data/*.md read at runtime — so
+# they need a server only because fetch() refuses file:// origins. Any static
+# server does; python is already a hard dependency here (build.py is python), so
+# there is no reason to reach for docker the way rig does.
+set -e
+
+SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+ROOT_DIR="$(dirname "$SCRIPT_DIR")"
+DOCS_DIR="$ROOT_DIR/docs"
+
+PYTHON="${PYTHON:-python3}"
+PORT="${DOCS_PORT:-8080}"
+
+serve() {
+    [ -n "${1:-}" ] && PORT="$1"
+    if [ ! -f "$DOCS_DIR/index.html" ]; then
+        echo "no docs/index.html" >&2
+        exit 1
+    fi
+    echo "docs on http://localhost:${PORT}/"
+    echo "  (ctrl-c to stop; nothing is installed and nothing persists)"
+    cd "$DOCS_DIR"
+    exec "$PYTHON" -m http.server "$PORT"
+}
+
+# Re-render docs/graphs/*.dot through every theme. The sources carry structure;
+# the palette lives in docs/graphs/themes/*.gvpr. See docs/graphs/README.md.
+graphs() {
+    if [ ! -x "$DOCS_DIR/graphs/render.sh" ]; then
+        echo "no docs/graphs/render.sh" >&2
+        exit 1
+    fi
+    exec bash "$DOCS_DIR/graphs/render.sh" "$@"
+}
+
+case "${1:-serve}" in
+    serve)       shift || true; serve "$@" ;;
+    graphs)      shift || true; graphs "$@" ;;
+    # `make docs 8090` is the obvious thing to type, so take it.
+    ''|*[!0-9]*) echo "usage: $0 [serve [port]|graphs [theme]]" >&2; exit 1 ;;
+    *)           serve "$1" ;;
+esac