diff --git a/bin/build_docs b/bin/build_docs new file mode 100644 index 0000000..596972b --- /dev/null +++ b/bin/build_docs @@ -0,0 +1,7 @@ +#!/bin/bash + +set -e +cd docs +rm -rf _build* +make html +cd ..