Or how about we add the version number to the <h1>, as in "DescripTor 1.6.0 API Documentation"? That's something that a few random other JavaDocs do that I just found on the internet. Patch:
Main headline is fine location, too.
Additional question is if the revision should be put anywhere? Thinking of people rolling their own versions, but just an idea.
Regarding the patch (which would also alter the title and only be in metrics-lib):
The version could be appended to the doctitle and be effective for all metrics-base using products, e.g., in base.xml
<javadoc destdir="${docs}" stylesheetfile="${javadocstyle}" footer="&copy; ${copyyear} The Tor Project"- doctitle="${javadoc-title}"+ doctitle="${javadoc-title} ${release.version}" overview="${basedir}/${resources}/overview.html" use="true" windowtitle="${javadoc-title}"> <classpath refid="classpath"/>
How about we add the revision to -dev versions only, but not to released versions? So, "DescripTor 1.6.0 API Documentation" and "DescripTor 1.6.0-dev 5b1db5d API Documentation"?
Speaking of, your patch appends the version as in: "DescripTor API Documentation 1.6.0-dev", but the version seems a bit out of place there at the end. How about we put together the doctitle in base.xml by using "${implementation-title} ${release-version} API Documentation", possibly with the option to override it? Plus the revision.