diff options
Diffstat (limited to '.github/scripts/check-header.py')
-rwxr-xr-x | .github/scripts/check-header.py | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/.github/scripts/check-header.py b/.github/scripts/check-header.py index ea37e04b7..a37411212 100755 --- a/.github/scripts/check-header.py +++ b/.github/scripts/check-header.py @@ -362,6 +362,9 @@ FREERTOS_IGNORED_PATTERNS = [ r'.*CMSIS.*', r'.*/makefile', r'.*/Makefile', + r'.*/trcConfig\.h.*', + r'.*/trcConfig\.c.*', + r'.*/trcSnapshotConfig\.h.*', ] FREERTOS_HEADER = [ |