Tomi Ollila <tomi.ollila@iki.fi> writes:
>
> Nice font, is that 20 pixels in height ? (and what font is it ?)

I use "DejaVu Sans Mono-normal-normal-normal-*-17-*-*-*-m-0-iso10646-1",
but I'm not sure what that is in pixels. Some random web types claim
that it is more like 23px @ 96 dpi.

>
>> Anyone else want to chime in before I apply this change?
>
> I personally tried with 12x25 sized font (xrandr tells 1920x1200, 
> 294mm x 165mm so what is that in dpi...) -- and it could be that
> majority of users uses smaller font so it could look a bit tall.
>
> Let's wait for a while for more comments.
>

Agreed, it's not too urgent. Although apparently the cool kids are
annoyed the old logo does not work with their themes.

d
_______________________________________________
notmuch mailing list -- notmuch@notmuchmail.org
To unsubscribe send an email to notmuch-leave@notmuchmail.org