summaryrefslogtreecommitdiff
path: root/make-man-index.py
diff options
context:
space:
mode:
authorLennart Poettering <lennart@poettering.net>2012-07-16 19:11:10 +0200
committerLennart Poettering <lennart@poettering.net>2012-07-16 19:11:10 +0200
commit051eaebb587d466ed21b51863d52d31fc1df57ca (patch)
tree79aecd1da9c42730e78bcbb9a158d37b2d1fba68 /make-man-index.py
parent6fa9a6109250d964db1f0690150b657db056ef81 (diff)
man: include number of man pages in index page
Diffstat (limited to 'make-man-index.py')
-rwxr-xr-xmake-man-index.py5
1 files changed, 5 insertions, 0 deletions
diff --git a/make-man-index.py b/make-man-index.py
index 364409025..44d15f8c2 100755
--- a/make-man-index.py
+++ b/make-man-index.py
@@ -52,4 +52,9 @@ for n in sorted(index.keys(), key = str.lower):
i = SubElement(li, 'i')
i.text = purpose
+hr = SubElement(body, 'hr')
+
+p = SubElement(body, 'p')
+p.text = "This index contains %s entries, referring to %i individual manual pages." % (len(index), len(argv)-1)
+
stdout.write(tostring(html))