From 559c2cfc4bf43cfa28d21cda75ca7e1e8bf02141 Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Tue, 23 Jan 2018 10:50:15 -0500
Subject: [PATCH] make `github_pages.sh` more chatty

---
 ci/github_pages.sh | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/ci/github_pages.sh b/ci/github_pages.sh
index 603b280f..f5dd7898 100644
--- a/ci/github_pages.sh
+++ b/ci/github_pages.sh
@@ -7,4 +7,6 @@ BOOK_DIR=book
 if [ "$TRAVIS_BRANCH" = master -a "$TRAVIS_PULL_REQUEST" = false ]; then
     mdbook build 
     ghp-import $BOOK_DIR
-fi
\ No newline at end of file
+else
+    echo Skipping 'mdbook build' because this is not master or this is just a PR.
+fi