Add script to update documentation website

foonathan · Oct 2, 2019 · c27b59c · c27b59c
1 parent 1eb9e77
commit c27b59c
Showing 1 changed file with 10 additions and 0 deletions.
diff --git a/doc/publish-docs.sh b/doc/publish-docs.sh
@@ -0,0 +1,10 @@
+#!/bin/sh
+# builds documentation and publishes it
+# run in root of repository, assumes `git worktree add doc/html gh-pages`
+
+doxygen doc/Doxyfile
+cd doc/html
+git add --all
+git commit -am"Update documentation"
+git push --force origin gh-pages
+