Thursday, June 26, 2008

Oops, nevermind about <BLANKLINE>

One should not post first thing in the morning, it seems. Avoiding use of <BLANKLINE> in doctests has nothing to do with whitespace normalization. :)