From: Zbigniew Jędrzejewski-Szmek Date: Thu, 14 Feb 2013 02:51:31 +0000 (-0500) Subject: man: add filenames to the index X-Git-Tag: v198~243 X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ianmdlvl/git?p=elogind.git;a=commitdiff_plain;h=a4e0b94d318e35b1441fc56f590668e80ff2e44e man: add filenames to the index Limiting the addition to filenames from seems to give a good enough S/N ratio. --- diff --git a/make-directive-index.py b/make-directive-index.py index b06a54c1d..15bd9b934 100755 --- a/make-directive-index.py +++ b/make-directive-index.py @@ -146,6 +146,15 @@ TEMPLATE = '''\ + + Files and directories + + Paths and file names referred to in the + documentation. + + + + Colophon @@ -162,10 +171,11 @@ def _extract_directives(directive_groups, formatting, page): t = tree.parse(page) section = t.find('./refmeta/manvolnum').text pagename = t.find('./refmeta/refentrytitle').text + + storopt = directive_groups['options'] for variablelist in t.iterfind('.//variablelist'): klass = variablelist.attrib.get('class') storvar = directive_groups[klass or 'miscellaneous'] - storopt = directive_groups['options'] #