Merge remote-tracking branch 'origin/master'

2017-05-15 09:47:19 +02:00 · 2017-05-15 09:47:19 +02:00 · 96641035d8
commit 96641035d8
parent a315cfa3af 1095829d9f
1 changed files with 3 additions and 1 deletions
--- 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