Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove Monaco font family altogether? #460

Closed
unthingable opened this issue Sep 12, 2017 · 1 comment
Closed

Remove Monaco font family altogether? #460

unthingable opened this issue Sep 12, 2017 · 1 comment
Assignees

Comments

@unthingable
Copy link

As many reporters of a similar problem have stated back in 2014, I am no font expert. Still, from my limited research it seems Monaco has no business being in the list of families for monospaced things, seeing that it has no bold variant and is not easily removable on MacOS Sierra. Chrome appears to have fixed this internally but Safari has not:

untitled

(as seen on http://docs.idris-lang.org/en/latest/st/state.html)

@Blendify Blendify added Needed: design decision A core team decision is required Support Support question labels Dec 17, 2017
@Blendify
Copy link
Member

Considering this is not even our main monospace font but a fallback for a couple of fallbacks I have no problem removing it. But would like to hear from @agjohnson and @ericholscher first.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants