[2.0] Font size if visibly bigger in the [new REPL window]

[dabrazhe]

See the image below. If you decrease font it also affects the code editor window, making it too small.

[PEZ]

Yes, there is currently a bug in vscode that prevents us from using the same font size as the editors. But I saw that the bug is being fixed, so hopefully, we can get rid of this problem soon.

[ncharchut]

Has this been resolved?

[PEZ]

No. This is a tricky one.

[ITSecMedia]

Any updates on this nasty bug?

[PEZ]

Actually, I spoke to some VS Code dev guys the other day, and they said they have provided what is needed to fix this. I haven't had the time to look at it yet, though. But there's hope!

[PEZ]

Turns out there isn't a nice way to do this: microsoft/vscode#86722

But I've sort of hacked my way around it now. Next release!

[elldritch]

On 2.0.68, I'm seeing some strange UI behaviour where my REPL is now in what looks like the default sans-serif font rather than my monospace editor font. Any idea how I can start debugging this?

[PEZ]

Indeed. I found where I had messed up and have fixed that in 2.0.69.