From 1095829d9ffe0ae7d7f729b7d516bdb873fe1e61 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Michal=20=C4=8Ciha=C5=99?= Date: Mon, 15 May 2017 09:46:45 +0200 Subject: [PATCH] Avoid linting removed files MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit We can not lint files which have been removed in the commit. Signed-off-by: Michal Čihař --- test/ci-lint | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/test/ci-lint b/test/ci-lint index 8dcd48f554..1e5e4959fb 100755 --- a/test/ci-lint +++ b/test/ci-lint @@ -7,5 +7,7 @@ else fi for FILE in $FILES ; do - php -l $FILE + if [ -f $FILE ] ; then + php -l $FILE + fi done