Always identify version of javadoc used to generate docs

Currently, the `-notimestamp` option suppresses both the timestamp that javadoc was run _and_ the version of javadoc that was used.

Being able to suppress the timestamp is useful for situations in which copies of the documentation will be compared and when the different timestamps are unnecessary differences. But, it is less clear that it is helpful to suppress the javadoc version string, and having the version string always available is useful for tools that want to analyze the output.