Variable pitch mode line

[Lars Ingebrigtsen]

It's been almost a month since it was switched to "on", so I think it's
about time to take stock.

I think that, long term, we want to go in that direction.  But we've
uncovered some usability problems, mainly in the "how do I click those
things in "U:--" anyway?" area, and we've got a plan to fix that, but
haven't yet.

So I think the way forward is to revert the trunk back to monospaced
fonts, then fix the usability problems, and then do another test in a
few months.

-- 
(domestic pets only, the antidote for overdose, milk.)
   bloggy blog: http://lars.ingebrigtsen.no