From 136b61ae70113922330de032f005b4acb50bc800 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 18 Feb 2019 13:28:59 +0100
Subject: Fix per-commit linting with bot merges

When the bot auto-merged the linter saw no commits to lint, eg
https://gitlab.com/coq/coq/-/jobs/162893603

I'm pushing from a non-current master so we will see if this works.
---
 dev/lint-repository.sh | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

(limited to 'dev')

diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh
index f588c20d02..2e8a7455de 100755
--- a/dev/lint-repository.sh
+++ b/dev/lint-repository.sh
@@ -9,10 +9,17 @@
 
 CODE=0
 
-# We assume that all merge commits are from the main branch
+if [[ $(git log -n 1 --pretty='format:%s') == "Bot merge"* ]]; then
+    # The FIRST parent of bot merges is from the PR, the second is
+    # current master
+    head=$(git rev-parse HEAD~)
+else
+    head=$(git rev-parse HEAD)
+fi
+
+# We assume that all non-bot merge commits are from the main branch
 # For Coq it is extremely rare for this assumption to be broken
-read -r base < <(git log -n 1 --merges --pretty='format:%H')
-head=$(git rev-parse HEAD)
+read -r base < <(git log -n 1 --merges --pretty='format:%H' "$head")
 
 dev/lint-commits.sh "$base" "$head" || CODE=1
 
-- 
cgit v1.2.3