Rename tools scripts

1 files changed, 14 insertions, 0 deletions

diff --git a/tools/docs-push-gh-pages b/tools/docs-push-gh-pages
new file mode 100755
index 0000000..36e80f8
--- /dev/null
+++ b/tools/docs-push-gh-pages
@@ -0,0 +1,14 @@
+#!/bin/bash
+
+./docs-generate
+cd ..
+git checkout gh-pages
+find . -maxdepth 1 -not -name "docs" -not -name ".git" -not -name "tools" -print0 | xargs -0 rm -r
+mv docs/* .
+mv docs/.nojekyll .
+rmdir docs
+rm -r tools/*
+git add -A
+git commit -m "Updated docs $(date)"
+git push origin gh-pages
+git checkout master