diff --git a/test/ci-lint b/test/ci-lint
index 8dcd48f5541c..1e5e4959fbed 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