It's just a pixel or two shorter now.  But that's probably because I'm
using a different font these days.

But, yes, we should have a look at how we choose this font and see
whether we can get a more precise height match.  It's going to be more
important if we're starting to use variable pitch faces more.

To return to the subject of filling -- I don't think we have enough
regularity in the doc strings to do that.  We've previously discussed (a
few years back) how to do paragraphs in doc strings, and we decided to
do that with an empty line -- but there's still tons of doc strings that
are formatted like:

----
This is the first paragraphs, and here's
the second line.
This is obviously the second paragraph, and
you can tell because of how that second line
was shorter, can't you?  Absolutely, you can.
And this is the third paragraph, and now
things get complicated.
----

So if we're going to fill, we'd have to audit the doc strings.  And
that's a huge job.  So I don't think we can do filling.

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