diff options
Diffstat (limited to 'doc/tools/make_rst.py')
| -rwxr-xr-x | doc/tools/make_rst.py | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/doc/tools/make_rst.py b/doc/tools/make_rst.py index 0649a0bb62..28d30a594d 100755 --- a/doc/tools/make_rst.py +++ b/doc/tools/make_rst.py @@ -607,10 +607,6 @@ def main() -> None: continue doc = tree.getroot() - if "version" not in doc.attrib: - print_error(f'{cur_file}: "version" attribute missing from "doc".', state) - continue - name = doc.attrib["name"] if name in classes: print_error(f'{cur_file}: Duplicate class "{name}".', state) |