Which looks like the same font for `variable-pitch' to me, only a lot
larger (since this is a HiDPI screen and the "fixed" font is tiny here).