[BLUEJ-1015] Editor: lines not drawn at correct size after changing font size, visual glitch
See attached screenshots: {quote} Increasing the size will cause some lines to overlay. Clicking on an affected line will fix it. Returning to the default size may keep a gap between two lines.{quote}
!1.png|thumbnail! !2.png|thumbnail! !3.png|thumbnail!
Tested on Windows 10 with HiDPI
Issue metadata
- Issue type: Bug
- Priority: Medium
- Fix versions: 4.5.0