I haven't been able to find a setting for specifying the gutter font size. When I change the default theme to use 10pt text, the gutter numbers look like they stay at 12 pt (although they line up properly). I have searched both the default theme and LeoPyRef, and haven't found it so far.
Pre-themes, I think it used the body font size. -- You received this message because you are subscribed to the Google Groups "leo-editor" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/leo-editor/78f6b384-e678-4c12-94e8-e028030ac346n%40googlegroups.com.
