Merge remote-tracking branch 'origin/master'

phpmyadmin · May 15, 2017 · 9664103 · 9664103
2 parents a315cfa + 1095829
commit 9664103
Showing 1 changed file with 3 additions and 1 deletion.
diff --git 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