diff options
Diffstat (limited to 'devtools')
| -rwxr-xr-x | devtools/check-forbidden-tokens.awk | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/devtools/check-forbidden-tokens.awk b/devtools/check-forbidden-tokens.awk index 026844141c..90d3a64f8e 100755 --- a/devtools/check-forbidden-tokens.awk +++ b/devtools/check-forbidden-tokens.awk @@ -58,8 +58,11 @@ BEGIN { for (i in deny_folders) { re = "^\\+\\+\\+ b/" deny_folders[i]; if ($0 ~ re) { - in_file = 1 - last_file = $0 + # Check only if the files are not part of SKIP_FILES + if (!(length(SKIP_FILES) && ($re ~ SKIP_FILES))) { + in_file = 1 + last_file = $0 + } } } } |