diff --git a/.circleci/config.yml b/.circleci/config.yml index dbed7e4..302c8e0 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -358,7 +358,7 @@ jobs: subcommand: docdep - run: command: | - git config --global user.email "me@cschwarz.com" + git config --global user.email "zreplbot@cschwarz.com" git config --global user.name "zrepl-github-io-ci" # https://circleci.com/docs/2.0/add-ssh-key/#adding-multiple-keys-with-blank-hostnames diff --git a/docs/publish.sh b/docs/publish.sh index 83d61d3..04e6932 100755 --- a/docs/publish.sh +++ b/docs/publish.sh @@ -1,6 +1,5 @@ #!/bin/bash -set -eo pipefail - +set -euo pipefail NON_INTERACTIVE=false DO_CLONE=false @@ -13,7 +12,7 @@ while getopts "ca" arg; do DO_CLONE=true ;; *) - echo invalid option + echo "invalid option '-$arg'" exit 1 ;; esac @@ -27,11 +26,6 @@ checkout_repo_msg() { echo "clone ${GHPAGESREPO} to ${PUBLICDIR}:" } -exit_msg() { - echo "error, exiting..." -} -trap exit_msg EXIT - if ! type sphinx-versioning >/dev/null; then echo "install sphinx-versioning and come back" exit 1 @@ -71,6 +65,9 @@ git reset --hard origin/master echo "cleaning GitHub pages repo" git rm -rf . +cat > .gitignore <