diff options
author | Lennart Poettering <lennart@poettering.net> | 2012-07-16 19:11:10 +0200 |
---|---|---|
committer | Lennart Poettering <lennart@poettering.net> | 2012-07-16 19:11:10 +0200 |
commit | 051eaebb587d466ed21b51863d52d31fc1df57ca (patch) | |
tree | 79aecd1da9c42730e78bcbb9a158d37b2d1fba68 | |
parent | 6fa9a6109250d964db1f0690150b657db056ef81 (diff) |
man: include number of man pages in index page
-rwxr-xr-x | make-man-index.py | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/make-man-index.py b/make-man-index.py index 3644090254..44d15f8c29 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)) |