diff options
| -rwxr-xr-x | update_github_page | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/update_github_page b/update_github_page new file mode 100755 index 00000000..6925354b --- /dev/null +++ b/update_github_page @@ -0,0 +1,11 @@ +#!/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 checkout gh-pages +git pull . master +git push +git checkout master +git push |