diff options
| author | coqbot-app[bot] | 2020-11-24 15:54:59 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-24 15:54:59 +0000 |
| commit | 80110dcfa2c52f719bfcce2b0b2b976de7faa174 (patch) | |
| tree | 2a88d382efa07187330b9533dc2dfd188bb12378 /dev | |
| parent | b4cc5fa61236b6c6d716d2cf19947022658bd570 (diff) | |
| parent | c3b260cfd5e74501aa0101b9e75f050bd6a3566d (diff) | |
Merge PR #13466: Fix linter: incorrect commit was picked in CI
Reviewed-by: ejgallego
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/lint-repository.sh | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh index 2e8a7455de..7701264ad1 100755 --- a/dev/lint-repository.sh +++ b/dev/lint-repository.sh @@ -9,10 +9,10 @@ CODE=0 -if [[ $(git log -n 1 --pretty='format:%s') == "Bot merge"* ]]; then - # The FIRST parent of bot merges is from the PR, the second is +if [[ $(git log -n 1 --pretty='format:%s') == "[CI merge]"* ]]; then + # The second parent of bot merges is from the PR, the first is # current master - head=$(git rev-parse HEAD~) + head=$(git rev-parse HEAD^2) else head=$(git rev-parse HEAD) fi |