Fonts Again

Hi,

I've recently upgraded my system from Ubuntu 14.04 to 18.04 and I'm using 
the exmh package included in this release (2.8.0-7).

Since the upgrade, exmh uses a quite large font which might be a hint at 
my age but I digress.
app-defaults select "fixed" as font and I have no font selected in my 
exmh-defaults.

This seems to result in the TrueType font DejaVuSansMono being used. Now 
exmh doesn't seem to have provisions for selecting TrueType fonts at all, 
so there's some fontconfig magic going on here.
I'm quite happy with this font, just the size could be a bit smaller but I 
have no clue how to achieve this result.

I've also tried to go the traditional way of selecting a bitmap font in my 
exmh-defaults like this:

*font: -misc-fixed-medium-r-semicondensed--12-110-75-75-c-60-iso8859-1
*fl_font: -misc-fixed-medium-r-semicondensed--12-110-75-75-c-60-iso8859-1

This results in the font size I'm looking for, but even though it should 
be a fixed width font, it isn't and therefore is unusable.

I don't want to mess with the fontconfig system defaults as I like the 
fonts and sizes in all other programs as they are right now.

Any ideas?

Thanks,
Bodo
-- 
Bodo Bellut          [email protected]         |     USE PGP!       +-----------+
Talstr. 8d           Fax/Mobile:   just ask  | (key via server    |\  O---m  /|
44267 Dortmund       Fon: +49-700-77-BELLUT  |  or on request)    |/---------\|
PGP: 768/FA18A639 AE 5A 47 40 5A A0 D6 15  8E 54 44 AA 8D DD 6E BD+-----------+