diff options
| -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)) |