summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rwxr-xr-xtools/docs-generate3
-rwxr-xr-xtools/docs-push-gh-pages5
2 files changed, 5 insertions, 3 deletions
diff --git a/tools/docs-generate b/tools/docs-generate
index 0caab1d..1453346 100755
--- a/tools/docs-generate
+++ b/tools/docs-generate
@@ -1,7 +1,8 @@
#!/bin/bash
+set -e
cd ..
-rm -rf doc docs
+rm -rf doc docs || true
doxygen
mv doc/html docs
touch docs/.nojekyll
diff --git a/tools/docs-push-gh-pages b/tools/docs-push-gh-pages
index 36e80f8..4d07dbd 100755
--- a/tools/docs-push-gh-pages
+++ b/tools/docs-push-gh-pages
@@ -1,13 +1,14 @@
#!/bin/bash
+set -e
./docs-generate
cd ..
git checkout gh-pages
-find . -maxdepth 1 -not -name "docs" -not -name ".git" -not -name "tools" -print0 | xargs -0 rm -r
+find . -maxdepth 1 -not -name "docs" -not -name ".git" -not -name "tools" -print0 | xargs -0 rm -r || true
mv docs/* .
mv docs/.nojekyll .
rmdir docs
-rm -r tools/*
+rm -r tools/* || true
git add -A
git commit -m "Updated docs $(date)"
git push origin gh-pages