diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/ci-common.sh | 2 | ||||
| -rwxr-xr-x | dev/lint-repository.sh | 2 |
2 files changed, 3 insertions, 1 deletions
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 05fa33e972..d7a356930e 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -19,6 +19,8 @@ else then export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER" export CI_BRANCH="$CIRCLE_BRANCH" + else # assume local + export CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" fi export COQBIN="$PWD/bin" fi diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh index e3ec51aeb6..ee9c8777a3 100755 --- a/dev/lint-repository.sh +++ b/dev/lint-repository.sh @@ -14,7 +14,7 @@ then # skip PRs from before the linter existed if [ -z "$(git ls-tree --name-only "${TRAVIS_PULL_REQUEST_SHA}" dev/lint-commits.sh)" ]; then - 2>&1 echo "Linting skipped: pull request older than the linter." + 1>&2 echo "Linting skipped: pull request older than the linter." exit 0 fi |