This doesn't apply cleanly because of #2140. However, I'm not sure what to do about that, as I feel like this one is way better than just setting the value manually to something to workaround the issue.
However, maybe there's another reason to want to increase the margin width regardless of the font size? Even then, I'd suggest then it would be better to make the ratio configurable rather than an absolute value again; but that would be an incompatible change, so I wonder what you guys think? @elextr @codebrainz @eht16 -- You are receiving this because you are subscribed to this thread. Reply to this email directly or view it on GitHub: https://github.com/geany/geany/pull/1738#issuecomment-706091629
