make github_pages.sh more chatty

nikomatsakis · nikomatsakis · commit 33c2b4c5f462 · 2018-01-23T10:50:31.000-05:00
diff --git 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
+else
+    echo Skipping 'mdbook build' because this is not master or this is just a PR.
+fi
