I'm using Ubuntu 20.04 and I still have this problem. I attached my filetypes.common here. I uncommented styling and added line_height=1;1;, but I still have this issue. I am using DejaVu Sans Mono with a font size of 11. I noticed that zooming in or increasing the size of the font resolves the issue, but I would like to stick to 11pt font.

Someone suggested changing the font to Nimbus Mono PS Regular, but I really dislike that font. If there are any alternative fonts that don't have issues, let me know.


You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub, or unsubscribe.