summaryrefslogtreecommitdiff
path: root/make-man-index.py
diff options
context:
space:
mode:
authorZbigniew Jędrzejewski-Szmek <zbyszek@in.waw.pl>2013-03-07 13:04:17 -0500
committerZbigniew Jędrzejewski-Szmek <zbyszek@in.waw.pl>2013-03-07 13:04:17 -0500
commit3c1872ebb6e9a435f61c3df0399a353ae28fb472 (patch)
tree7c20046a398daadd23381e9a377da97783467aff /make-man-index.py
parent7ba9719595ee13612c9aea786233ffdd4d77ee46 (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-xmake-man-index.py7
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())