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.