From c3b260cfd5e74501aa0101b9e75f050bd6a3566d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 24 Nov 2020 15:04:05 +0100
Subject: Fix linter: incorrect commit was picked in CI

The bot merge was changed some time ago.
---
 dev/lint-repository.sh | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'dev')

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
-- 
cgit v1.2.3