From f1168b816dcbd8ee45787da1251ba5b2a68176d5 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Wed, 6 Dec 2017 14:16:08 +0100
Subject: Linter: skip PRs older than the linter.

---
 dev/lint-repository.sh | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'dev/lint-repository.sh')

diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh
index ecf7880e2..87a829746 100755
--- a/dev/lint-repository.sh
+++ b/dev/lint-repository.sh
@@ -11,6 +11,13 @@ CODE=0
 
 if [ "(" "-n" "${TRAVIS_PULL_REQUEST}" ")" "-a" "(" "${TRAVIS_PULL_REQUEST}" "!=" "false" ")" ];
 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."
+        exit 0
+    fi
+
     # Some problems are too widespread to fix in one commit, but we
     # can still check that they don't worsen.
     CUR_HEAD=${TRAVIS_COMMIT_RANGE%%...*}
-- 
cgit v1.2.3