diff options
| author | Sylvain Henry <sylvain@haskus.fr> | 2019-12-21 14:18:21 +0100 |
|---|---|---|
| committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2019-12-25 19:23:54 -0500 |
| commit | aeea92ef6ffa514793b1d37b38aaed3616c5c24a (patch) | |
| tree | ef6a8fa21ec1276d522b0c66de3cc11970dcb3a1 /.gitlab | |
| parent | 40327b037f7115f7b05cc0265acb787671bea294 (diff) | |
| download | haskell-aeea92ef6ffa514793b1d37b38aaed3616c5c24a.tar.gz | |
Switch to ReadTheDocs theme for the user-guide
Diffstat (limited to '.gitlab')
| -rwxr-xr-x | .gitlab/linters/check-cpp.py | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/.gitlab/linters/check-cpp.py b/.gitlab/linters/check-cpp.py index c51c127379..5377fcb005 100755 --- a/.gitlab/linters/check-cpp.py +++ b/.gitlab/linters/check-cpp.py @@ -26,6 +26,9 @@ for l in linters: l.add_path_filter(lambda path: path != Path('docs', 'coding-style.html')) # Don't lint vendored code l.add_path_filter(lambda path: not path.name == 'config.guess') + # Don't lint font files + l.add_path_filter(lambda path: not path.parent == Path('docs','users_guide', + 'rtd-theme', 'static', 'fonts')) if __name__ == '__main__': run_linters(linters) |