scrpit to push docs

docs/build.sh

@@ -0,0 +1,23 @@
+#! /bin/bash
+
+REMOTE=origin
+
+set -e
+
+if ! [ -f "./src/SUMMARY.md" ]; then
+    echo "Run this from the docs/ dir"
+    exit 1
+fi
+
+if ! [ -d ./tmp ]; then
+    git worktree add tmp gh-pages
+fi
+
+(cd tmp && git pull $REMOTE gh-pages)
+
+rm -rf tmp/*
+mdbook build
+cp -rp book/* tmp
+(cd tmp && git add -A)
+(cd tmp && git commit -am "update docs")
+(cd tmp && git push $REMOTE gh-pages:gh-pages)