diff --git a/ci/github_pages.sh b/ci/github_pages.sh index 4a45b145..f96aefc7 100644 --- a/ci/github_pages.sh +++ b/ci/github_pages.sh @@ -37,14 +37,14 @@ git config user.name "Michael Bryan" git config user.email "michaelfbryan@gmail.com" git remote add upstream "https://$GH_TOKEN@github.com/rust-lang-nursery/mdBook.git" -git fetch upstream -git reset upstream/gh-pages +git fetch upstream --quiet +git reset upstream/gh-pages --quiet touch . echo -e "${CYAN}Pushing changes to gh-pages${NC}" -git add -A . -git commit -m "rebuild pages at ${rev}" -git push -q upstream HEAD:gh-pages +git add -A . --quiet +git commit -m "rebuild pages at ${rev}" --quiet +git push -q upstream HEAD:gh-pages --quiet echo -e "${GREEN}Deployed docs to GitHub Pages${NC}"