diff options
| -rwxr-xr-x | update_github_page | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/update_github_page b/update_github_page deleted file mode 100755 index 5573bf4d..00000000 --- a/update_github_page +++ /dev/null @@ -1,11 +0,0 @@ -#!/bin/bash -# -# Github populates http://akkartik.github.io/mu with branch gh-pages -# (More info: https://pages.github.com) -# We keep gh-pages sync'd with master. - -git push || exit 1 -git checkout gh-pages -git pull . master -git push -git checkout master |