diff options
Diffstat (limited to 'tools/checkAPIs.pl')
-rwxr-xr-x | tools/checkAPIs.pl | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/tools/checkAPIs.pl b/tools/checkAPIs.pl index 5a9da1131d..90da6e1713 100755 --- a/tools/checkAPIs.pl +++ b/tools/checkAPIs.pl @@ -1935,7 +1935,10 @@ while ($_ = $ARGV[0]) # delete leading './' $filename =~ s{ ^ \. / } {}xo; - + unless (-f $filename) { + print STDERR "Warning: $filename is not of type file - skipping.\n"; + next; + } # Read in the file (ouch, but it's easier that way) open(FC, $filename) || die("Couldn't open $filename"); $line = 1; |