diff options
| -rwxr-xr-x | make-man-index.py | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/make-man-index.py b/make-man-index.py index e09d62a5e8..3644090254 100755 --- a/make-man-index.py +++ b/make-man-index.py @@ -42,11 +42,14 @@ for n in sorted(index.keys(), key = str.lower): ul = SubElement(body, 'ul') ul.set('style', 'list-style-type:none') - li = SubElement(ul, 'li'); + li = SubElement(ul, 'li') - a = SubElement(li, 'a'); + a = SubElement(li, 'a') a.set('href', path) a.text = n + '(' + section + ')' - a.tail = ' -- ' + purpose + a.tail = ' -- ' + + i = SubElement(li, 'i') + i.text = purpose stdout.write(tostring(html)) |