Update code_lint.py (#4470)

This commit is contained in:
Jack Gerrits 2024-12-02 16:42:28 -05:00 committed by GitHub
parent 1b58f6e7d5
commit 732391859d
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194

View File

@ -51,7 +51,7 @@ class CodeLinter(Builder):
def write_doc(self, docname: str, doctree: nodes.Node) -> None:
path_prefix: str = self.app.config.code_lint_path_prefix
supported_languages = set(["python"])
supported_languages = set(["python", "default"])
if not docname.startswith(path_prefix):
return