On Tue, 14 May 2024 22:25:13 GMT, Jonathan Gibbons <j...@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

Reply via email to