diff options
Diffstat (limited to 'src/doc/rustc-dev-guide/ci/github_pages.sh')
| -rw-r--r-- | src/doc/rustc-dev-guide/ci/github_pages.sh | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/src/doc/rustc-dev-guide/ci/github_pages.sh b/src/doc/rustc-dev-guide/ci/github_pages.sh deleted file mode 100644 index ffd89ad5227..00000000000 --- a/src/doc/rustc-dev-guide/ci/github_pages.sh +++ /dev/null @@ -1,11 +0,0 @@ -#!/bin/bash -set -ex - -BOOK_DIR=book - -# Only upload the built book to github pages if it's a commit to master -if [ "$TRAVIS_BRANCH" = master -a "$TRAVIS_PULL_REQUEST" = false ]; then - mdbook build -else - echo Skipping 'mdbook build' because this is not master or this is just a PR. -fi |