VS Code renders a character wrong?

Stream: general

[Alex Meiburg]

Confusingly, it seems as though - with the default font - VS Code renders \^varphi ᵠ as if it were a psi.
image.png
It is the "open variant", but this is clearly a psi, not a phi!

Second image: the superscript varphi, phi, varphi, and psi. It's literally the same glyph scaled down.
image.png

[Alex Meiburg]

I know that this is the Lean Zulip and not a VS Code support group... but I figured that probably this is not a common issue to run into in many other languages.

[Alex Meiburg]

Ironically, there is no superscript psi, although there will be in Unicode 18 (come September). It was the character I wanted to use. But I chose superscript varphi as the closest approximation. Then when I typed it, I was met with this nonsense.

[Alex Meiburg]

Oddly, the tooltip renders it correctly. So maybe there's something weirder.
image.png

[Eric Wieser]

Which font is this? "Default font" changes by system

[Marc Huisinga]

(vscode-lean4#584 - most likely a font issue)

[Martin Dvořák]

Just move to JuliaMono, like most of us did.