Merge PR #13466: Fix linter: incorrect commit was picked in CI

Reviewed-by: ejgallego
coq · Nov 24, 2020 · 80110dc · 80110dc
2 parents b4cc5fa + c3b260c
commit 80110dc
Showing 1 changed file with 3 additions and 3 deletions.
diff --git 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