diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/make-man-rules.py | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/tools/make-man-rules.py b/tools/make-man-rules.py index 0d1ca244c4..6224de3cc0 100644 --- a/tools/make-man-rules.py +++ b/tools/make-man-rules.py @@ -66,6 +66,8 @@ def xml(file): def add_rules(rules, name): xml = xml_parse(name) # print('parsing {}'.format(name), file=sys.stderr) + if xml.getroot().tag != 'refentry': + return conditional = xml.getroot().get('conditional') or '' rulegroup = rules[conditional] refmeta = xml.find('./refmeta') @@ -86,7 +88,11 @@ def create_rules(xml_files): " {conditional => {alias-name => source-name}} " rules = collections.defaultdict(dict) for name in xml_files: - add_rules(rules, name) + try: + add_rules(rules, name) + except Exception: + print("Failed to process", name, file=sys.stderr) + raise return rules def mjoin(files): |