summaryrefslogtreecommitdiff
path: root/doc/doc-txt
diff options
context:
space:
mode:
authorPhilip Hazel <ph10@hermes.cam.ac.uk>2005-02-17 12:17:09 +0000
committerPhilip Hazel <ph10@hermes.cam.ac.uk>2005-02-17 12:17:09 +0000
commita82639d214617fffa4df4af3b733224e3dd81c11 (patch)
tree90106fc0bdeea14263dc75b2886237fbe3977f09 /doc/doc-txt
parent8e669ac162fe3b1040297f1d021de10778dce9d9 (diff)
Fix problems in the script that makes HTML documents: (1) The new "Use"
item for options wasn't being properly processed; (2) tidy section titles (no dot after chap.sect).
Diffstat (limited to 'doc/doc-txt')
0 files changed, 0 insertions, 0 deletions