1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
#!/usr/bin/env python
"Update the command index in index.html."
import os
commands = []
reffiles = {}
for infile in os.listdir('.'):
if not infile.endswith('.html'): continue
for part in open(infile).read().split('<a name="')[1:]:
command = part.split('"')[0]
commands.append(command)
reffiles[command] = infile
commands.sort()
head, trash, tail = open('index.html').read().split('SCRIPT')
f = open('index.html', 'w')
f.write(head + 'SCRIPT -->\n')
for command in commands:
f.write('<dt><a href="' + reffiles[command] + '#' + command + '">' + command + '</a></dt>\n')
f.write('<dd></dd>\n')
f.write('<!-- SCRIPT' + tail)
|
