nomeata / incredible

The Incredible Proof Machine
MIT License
358 stars 36 forks source link

Font problem: 'sans' /= 'sans-serif' #112

Closed NoLongerBreathedIn closed 5 years ago

NoLongerBreathedIn commented 5 years ago

On line 207 of webui/shapes.js, a font family is given as 'sans'. I suggest changing it to 'sans-serif', as this leads to more consistent display of text (also, on my system, 'sans' (but not 'sans-serif') displays as DejaVu Sans, which I personally find ugly).