diff options
| author | Rémi Verschelde <remi@verschelde.fr> | 2022-06-11 10:51:03 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-06-11 10:51:03 +0200 |
| commit | d62cb0e571ef715afc2fa5d9533b2e8d8a19cc8b (patch) | |
| tree | b97ea3bba88e5f233cc55ebca2f168605cfd1040 /doc | |
| parent | bc30eefeb48e47d96bffe01de053268f8202e060 (diff) | |
| parent | 1163af17567c1391f7c36d553b4d1414f3bc6c57 (diff) | |
Merge pull request #61917 from Calinou/makerst-fix-error-reporting
Diffstat (limited to 'doc')
| -rwxr-xr-x | doc/tools/make_rst.py | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/tools/make_rst.py b/doc/tools/make_rst.py index 2e227ce578..aaccbd7aa9 100755 --- a/doc/tools/make_rst.py +++ b/doc/tools/make_rst.py @@ -464,17 +464,17 @@ def main(): # type: () -> None try: tree = ET.parse(cur_file) except ET.ParseError as e: - print_error("{}.xml: Parse error while reading the file: {}".format(cur_file, e), state) + print_error("{}: Parse error while reading the file: {}".format(cur_file, e), state) continue doc = tree.getroot() if "version" not in doc.attrib: - print_error('{}.xml: "version" attribute missing from "doc".'.format(cur_file), state) + print_error('{}: "version" attribute missing from "doc".'.format(cur_file), state) continue name = doc.attrib["name"] if name in classes: - print_error('{}.xml: Duplicate class "{}".'.format(cur_file, name), state) + print_error('{}: Duplicate class "{}".'.format(cur_file, name), state) continue classes[name] = (doc, cur_file) |