diff options
author | Zbigniew Jędrzejewski-Szmek <zbyszek@in.waw.pl> | 2013-03-07 13:04:17 -0500 |
---|---|---|
committer | Zbigniew Jędrzejewski-Szmek <zbyszek@in.waw.pl> | 2013-03-07 13:04:17 -0500 |
commit | 3c1872ebb6e9a435f61c3df0399a353ae28fb472 (patch) | |
tree | 7c20046a398daadd23381e9a377da97783467aff /make-man-index.py | |
parent | 7ba9719595ee13612c9aea786233ffdd4d77ee46 (diff) |
build-sys: check if manpage ids match file names
Commit ed1553a fixed current errors, but this error is easy to
make. A wrong id messes up the indexes and linking, so it is
better to catch this automatically.
Diffstat (limited to 'make-man-index.py')
-rwxr-xr-x | make-man-index.py | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/make-man-index.py b/make-man-index.py index f829d98b6..d38d5b63f 100755 --- a/make-man-index.py +++ b/make-man-index.py @@ -21,6 +21,7 @@ import collections import xml.etree.ElementTree as tree import sys +import re MDASH = ' — ' if sys.version_info.major >= 3 else ' -- ' TEMPLATE = '''\ @@ -66,10 +67,16 @@ SUMMARY = '''\ COUNTS = '\ This index contains {count} entries, referring to {pages} individual manual pages.' +def check_id(page, t): + id = t.getroot().get('id') + if not re.search('/' + id + '[.]', page): + raise ValueError("id='{}' is not the same as page name '{}'".format(id, page)) + def make_index(pages): index = collections.defaultdict(list) for p in pages: t = tree.parse(p) + check_id(p, t) section = t.find('./refmeta/manvolnum').text refname = t.find('./refnamediv/refname').text purpose = ' '.join(t.find('./refnamediv/refpurpose').text.split()) |