Fix problems in the script that makes HTML documents: (1) The new "Use"
authorPhilip Hazel <ph10@hermes.cam.ac.uk>
Thu, 17 Feb 2005 12:17:09 +0000 (12:17 +0000)
committerPhilip Hazel <ph10@hermes.cam.ac.uk>
Thu, 17 Feb 2005 12:17:09 +0000 (12:17 +0000)
commita82639d214617fffa4df4af3b733224e3dd81c11
tree90106fc0bdeea14263dc75b2886237fbe3977f09
parent8e669ac162fe3b1040297f1d021de10778dce9d9
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).
doc/doc-scripts/g2h