diff options
| -rwxr-xr-x | tool/leaked-globals | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tool/leaked-globals b/tool/leaked-globals index ee75f78d1d..3e3bda5632 100755 --- a/tool/leaked-globals +++ b/tool/leaked-globals @@ -47,7 +47,9 @@ if platform and !platform.empty? end missing = File.dirname(config) + "/missing/" ARGV.reject! do |n| - unless (src = Dir.glob(missing + File.basename(n, ".*") + ".[cS]")).empty? + base = File.basename(n, ".*") + next true if REPLACE.include?(base) + unless (src = Dir.glob(missing + base + ".[cS]")).empty? puts "Ignore #{col.skip(n)} because of #{src.map {|s| File.basename(s)}.join(', ')} under missing" true end |