Add publish-docs

1 files changed, 38 insertions, 0 deletions

diff --git a/publish-docs b/publish-docs
new file mode 100755
index 0000000..ab0622a
--- /dev/null
+++ b/publish-docs
@@ -0,0 +1,38 @@
+#!/bin/sh
+
+set -eu
+
+build_docs()
+{
+    local srcdir="$1"
+    local log="$(mktemp)"
+    
+    set -eu
+    cd "$srcdir"/doc
+    if make dirhtml > "$log" 2>&1
+    then
+        echo "$srcdir/doc/_build/dirhtml"
+        rm -f "$log"
+    else
+        cat "$log" 1>&2
+        rm -f "$log"
+        exit 1
+    fi
+}
+
+tarballurl="$1"
+rsync_target="$2"
+
+tempdir="$(mktemp -d)"
+trap 'rm -rf "$tempdir"' EXIT INT
+
+echo "Downloading and unpacking sources"
+wget -O- -q "$tarballurl" | tar -C "$tempdir" -xzf -
+
+echo "Building docs"
+docdir=$(build_docs "$tempdir"/*/.)
+
+echo "Uploading docs"
+rsync -ahHS --delete "$docdir/." "$rsync_target/."
+
+#find "$tempdir" -mindepth 1 -delete