diff options
Diffstat (limited to 'update_github_page')
| -rwxr-xr-x | update_github_page | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/update_github_page b/update_github_page index 6925354b..4a3dd003 100755 --- a/update_github_page +++ b/update_github_page @@ -4,8 +4,8 @@ # (More info: https://pages.github.com) # We keep gh-pages sync'd with master. +git push git checkout gh-pages git pull . master git push git checkout master -git push |