mirror of
https://github.com/systemd/systemd-stable.git
synced 2025-02-02 09:47:03 +03:00
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.
This commit is contained in:
parent
7ba9719595
commit
3c1872ebb6
@ -21,6 +21,7 @@
|
|||||||
import collections
|
import collections
|
||||||
import xml.etree.ElementTree as tree
|
import xml.etree.ElementTree as tree
|
||||||
import sys
|
import sys
|
||||||
|
import re
|
||||||
MDASH = ' — ' if sys.version_info.major >= 3 else ' -- '
|
MDASH = ' — ' if sys.version_info.major >= 3 else ' -- '
|
||||||
|
|
||||||
TEMPLATE = '''\
|
TEMPLATE = '''\
|
||||||
@ -66,10 +67,16 @@ SUMMARY = '''\
|
|||||||
COUNTS = '\
|
COUNTS = '\
|
||||||
This index contains {count} entries, referring to {pages} individual manual pages.'
|
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):
|
def make_index(pages):
|
||||||
index = collections.defaultdict(list)
|
index = collections.defaultdict(list)
|
||||||
for p in pages:
|
for p in pages:
|
||||||
t = tree.parse(p)
|
t = tree.parse(p)
|
||||||
|
check_id(p, t)
|
||||||
section = t.find('./refmeta/manvolnum').text
|
section = t.find('./refmeta/manvolnum').text
|
||||||
refname = t.find('./refnamediv/refname').text
|
refname = t.find('./refnamediv/refname').text
|
||||||
purpose = ' '.join(t.find('./refnamediv/refpurpose').text.split())
|
purpose = ' '.join(t.find('./refnamediv/refpurpose').text.split())
|
||||||
|
Loading…
x
Reference in New Issue
Block a user