But still, how can I reduce leo's font size with a theme applied w/o modifying the theme outline itself? Playing with `@string font-size`is still gives absolutely nothing. In my opinion the inability to change font size easily is the great miss of leo's styling. Cause default fonts are INCREDIBLY huge.
вт, 22 дек. 2020 г. в 22:35, Edward K. Ream <[email protected]>: > > > On Tue, Dec 22, 2020 at 11:21 AM [email protected] <[email protected]> > wrote: > >> I'm currently using >> >> @string font-family = Consolas, Droid Sans Mono, DejaVu Sans Mono >> >> I think that that Consolas comes with Windows and I like it better than >> some of the alternatives. Apparently it can be installed on Linux in some >> manner. I should probably move the DajaVu font ahead of the Droid, but at >> any rate this setting seems to work all right on both Windows and Linux. >> > > Thanks for these comments. Consolas does look fairly good. > > Devs, please feel free to change the font setting as you please in your > own themes. > > Edward > > -- > 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/CAMF8tS0woyZXozs7YMwwpLdri9-Uf4p6%2Bg_TExMevotVmygnWw%40mail.gmail.com > <https://groups.google.com/d/msgid/leo-editor/CAMF8tS0woyZXozs7YMwwpLdri9-Uf4p6%2Bg_TExMevotVmygnWw%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- 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/CAC%2B8SVwNjwz3vqTmE7%2BYQcROhqO9UnoxW%3D_q7vrji%3DDboQL-Lw%40mail.gmail.com.
