Pluto.jl: Header font for 0123456789 is too artsy

[Moelf]

I personally have 2 "complaints":

1. the 1 is confusing
2. the "baseline" is weird for this font. <--- less of an issue

[fonsp]

The 2 complaints are both just about the 10 digits, right?

[fonsp]

I am going to assume that it is, and otherwise refer to #2

[fonsp]

The typeface contains variants that solve these problems:

http://vollkorn-typeface.com/

but these are not included in the google-fonts-compiled version
https://fonts.google.com/specimen/Vollkorn

(which we get from
https://github.com/fontsource/fontsource/tree/master/packages/vollkorn
to avoid CDN issues)

The solution could be to use the original fonts:
https://github.com/FAlthausen/Vollkorn-Typeface

but these still need to be compiled to WOFF2:
https://github.com/google/woff2

We can then host them on our own fork of the Vollkorn repo, tag a release, and get them from jsdelivr

[fonsp]

The fork is here:
https://github.com/fonsp/Vollkorn-Typeface
if anyone wants to contribute

[pankgeorg]

@fonsp opened a PR to your fork

[fonsp]

Thanks to @pankgeorg for compiling!

Available at:
https://cdn.jsdelivr.net/gh/fonsp/Vollkorn-Typeface@1/fonts/woff2/Vollkorn-Regular.woff2

demo:
https://fonsp.com/Vollkorn-Typeface/fonts/woff2/index.html

[Moelf]

I'm fine with anything but the first. personally like the second one

[pankgeorg]

Opened a PR that uses the second one. I think the third is for tables (kind-of-fixed witdth?)

I love the slashed zero, but it fits in tables/codeblocks (the JuliaMono dotted zero triggers my trypophobia I think)