This only acknowledges some changes that have been in the publised version for ages already. It also gets rid of the minor version discrepancy between HTML and PostScript versions.