Mac fonts

Stream: general

[Jeremy Avigad]

I am teaching a summer school and someone here is having trouble with fonts on the Mac -- when she types "#check 2", the blackboard bold N doesn't appear. Does anyone know how to fix this?

[Bryan Gin-ge Chen]

Maybe some of the font recommendations in this thread will work?

[Scott Morrison]

Assuming she is using VS Code:
1. Press ⌘, to open preferences.
2. Type font family in the search box.
3. Try changing the defaults to Menlo, Monaco, 'Courier New', monospace.

[Jeremy Avigad]

Oh, sorry, I should have been more specific. It is the first day, and she is using the browser javascript version, with Chrome. (But the VS Code information is also helpful!)

[Dawn Jiang]

Thanks so much for the instructions! It works now:)

[Alexander Bentkamp]

I'am also missing some symbols on Mac, e.g. the subscript "l" in →ₗ[γ]. Has anyone figured out how to get that?

[Bryan Gin-ge Chen]

The steps that worked for me (from the thread linked above) were to install the Deja vu fonts and then change the list of fonts in VS code to DejaVu Sans Mono, Menlo, Monaco, 'Courier New', monospace

[Chris Hughes]

I use everson mono on mac. You have to download that, but all the unicode characters are monospace, which is nice.

[Alexander Bentkamp]

Very cool, thanks!