Export {HTML, PDF} options reduce font size, hard to read

[ekzhang]

I noticed when exporting notebooks that the exported .html and .pdf files would have very small font, which made it hard to read compared to the notebook viewed in the browser. The headings and figures remain the same size, but for some reason the font size for regular text (in rendered Markdown) and code changes.

At first I thought this was a rendering bug, but it turns out that by default font-size: 17px is set, yet for some reason, hide-ui.css overrides it to 14px.

Pluto.jl/frontend/hide-ui.css

Line 6 in b53d282

font-size: 14px;

Is there a reason why 17px would not be preferred for text in the exported files as well?

[fonsp]

Wow no that's a mistake - well found! Thanks!

[ekzhang]

Thanks for the quick reply! I'll test the changes & make a PR.