diff options
author | Tamar Christina <tamar@zhox.com> | 2021-07-31 14:35:01 +0100 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2021-12-14 20:50:47 -0500 |
commit | 8a2de3c295055771cb61606d599af63e61e420f4 (patch) | |
tree | ab0c535943a84cd46639a15c4ed33dbc4ebfd4db /.gitlab | |
parent | 9ff54ea8260b1b1508a19e968eb4584cb5cef93c (diff) | |
download | haskell-8a2de3c295055771cb61606d599af63e61e420f4.tar.gz |
rts: update xxhash used by the linker's hashmap
Diffstat (limited to '.gitlab')
-rwxr-xr-x | .gitlab/linters/check-cpp.py | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/.gitlab/linters/check-cpp.py b/.gitlab/linters/check-cpp.py index f904d81f8b..ffa430e10d 100755 --- a/.gitlab/linters/check-cpp.py +++ b/.gitlab/linters/check-cpp.py @@ -27,6 +27,8 @@ for l in linters: l.add_path_filter(lambda path: path != Path('docs', 'users_guide', 'utils.rst')) # Don't lint vendored code l.add_path_filter(lambda path: not path.name == 'config.guess') + # Don't lint files from external xxhash projects + l.add_path_filter(lambda path: path != Path('rts', 'xxhash.h')), # Don't lint font files l.add_path_filter(lambda path: not path.parent == Path('docs','users_guide', 'rtd-theme', 'static', 'fonts')) |