From 0816eb78b469994c645cda6578b1db8e49ddd75b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 8 Feb 2018 17:20:20 +0100
Subject: Fix redirection to stderr in lint-repository error message.

---
 dev/lint-repository.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh
index e3ec51aeb6..ee9c8777a3 100755
--- a/dev/lint-repository.sh
+++ b/dev/lint-repository.sh
@@ -14,7 +14,7 @@ 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."
+        1>&2 echo "Linting skipped: pull request older than the linter."
         exit 0
     fi
 
-- 
cgit v1.2.3