RFR: 8329617: Update stylesheet for specs and tool documentation

[Hannes Wallnöfer]

On Tue, 14 May 2024 22:25:13 GMT, Jonathan Gibbons <jjg at openjdk.org> wrote:

> Is there a reason to want the main font size to be different between the API pages and spec pages?

I did not want to change the font size in this patch. I started by changing the font size to 14 px, but went back to the initial 10 pt in order to detect any unintentional changes. To me the specs/man pages look good with the original font size, so I kept it that way. We can increase it if we think it's too small.

> FWIW, while the PR description says the body font size is 10pt vs 14px, on representative text for the `jdk.javadoc` module and Doc Comment Spec, I observed 13.333px vs 14px.

That's expected, as [10 pt corresponds to 13.33 px](https://cssunitconverter.com/pt-to-px/).

-------------

PR Comment: https://git.openjdk.org/jdk/pull/18694#issuecomment-2112330586