diff options
| author | Kartik K. Agaram <vc@akkartik.com> | 2015-05-14 16:05:24 -0700 |
|---|---|---|
| committer | Kartik K. Agaram <vc@akkartik.com> | 2015-05-14 16:05:24 -0700 |
| commit | 7234483b1cfb0afee10b61491a4024dcee7d5e43 (patch) | |
| tree | 9c21ff5bc5de81953afdd07782791f27c4c5301d /update_github_page | |
| parent | 65361948ca7975553757a0e0df4ac7352413044c (diff) | |
| download | mu-7234483b1cfb0afee10b61491a4024dcee7d5e43.tar.gz | |
1377 - handle github errors
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 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 |