Rename tools scripts

1 files changed, 0 insertions, 14 deletions

diff --git a/tools/push-ghpages b/tools/push-ghpages
deleted file mode 100755
index e7b41fa..0000000
--- a/tools/push-ghpages
+++ /dev/null
@@ -1,14 +0,0 @@
-#!/bin/bash
-
-./generate-docs
-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