[FR] Simpler file ID links in HTML export

[Nicholas Coltharp]

Exporting an ID link to HTML produces a link of the form <a 
href="file.html#id>. This makes sense if linking to a section ID. However, in 
the case of a file ID, the #id part is unnecessary, and in fact a file ID does 
not occur anywhere in the exported file. I wonder if it would be reasonable to 
simply remove the #id part in links to files.