From 7234483b1cfb0afee10b61491a4024dcee7d5e43 Mon Sep 17 00:00:00 2001 From: "Kartik K. Agaram" Date: Thu, 14 May 2015 16:05:24 -0700 Subject: 1377 - handle github errors --- update_github_page | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'update_github_page') 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 -- cgit 1.4.1-2-gfad0