Update tools scripts

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