diff options
author | Jiri Suchan <yed@vanyli.net> | 2022-08-23 22:21:46 +0900 |
---|---|---|
committer | Jiri Suchan <yed@vanyli.net> | 2022-09-30 19:03:17 +0700 |
commit | c5bd2f9dce17f3e6bf7d9681243e2743633db6f0 (patch) | |
tree | 5cc835252cc999d086deaf05f3821ef3ce9e37e8 /doc/translations | |
parent | f47979f0874b2ca6134e71575fbb359c6cc5ced0 (diff) |
ci: add Python static analysis check via mypy
Diffstat (limited to 'doc/translations')
-rw-r--r-- | doc/translations/extract.py | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/translations/extract.py b/doc/translations/extract.py index 5708e0072d..ce645436d9 100644 --- a/doc/translations/extract.py +++ b/doc/translations/extract.py @@ -60,7 +60,7 @@ BASE_STRINGS = [ ## <xml-line-number-hack from="https://stackoverflow.com/a/36430270/10846399"> import sys -sys.modules["_elementtree"] = None +sys.modules["_elementtree"] = None # type: ignore import xml.etree.ElementTree as ET ## override the parser to get the line number |