make `github_pages.sh` more chatty

2018-01-23 10:50:15 -05:00 · 2018-01-23 10:50:15 -05:00 · 559c2cfc4b
parent aee56ee555
commit 559c2cfc4b
1 changed files with 3 additions and 1 deletions
--- 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