From 016260eaf20f3fd06f9d29acbfea528012be1aa0 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Tue, 23 Jan 2018 10:50:15 -0500 Subject: [PATCH] make `github_pages.sh` more chatty --- src/doc/rustc-dev-guide/ci/github_pages.sh | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/doc/rustc-dev-guide/ci/github_pages.sh b/src/doc/rustc-dev-guide/ci/github_pages.sh index 603b280f9839..f5dd7898ba32 100644 --- 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 \ No newline at end of file +else + echo Skipping 'mdbook build' because this is not master or this is just a PR. +fi