make github_pages.sh more chatty

2018-01-23 10:50:15 -05:00 · 2018-01-23 10:50:15 -05:00 · 016260eaf2
commit 016260eaf2
parent 33893a8d5b
1 changed files with 3 additions and 1 deletions
--- a/src/doc/rustc-dev-guide/ci/github_pages.sh
+++ b/src/doc/rustc-dev-guide/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