The HTML files in here originally said "!--THIS IS A GENERATED FILE. DO NOT EDIT (2)-->".  It seems they were once produced by doclist.xsl from doclist.xml, but we've been editing the HTML files without realizing that.