diff options
| -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 4a3dd003..5573bf4d 100755 --- a/update_github_page +++ b/update_github_page @@ -4,7 +4,7 @@ # (More info: https://pages.github.com) # We keep gh-pages sync'd with master. -git push +git push || exit 1 git checkout gh-pages git pull . master git push |