On Wed, Jan 28, 2009 at 5:27 AM, Michał Trybus wrote:

Well, that's too bad. Sorry, my mistake. I hope it's ok now

Pushed, thanks. (On a side note, I noticed but didn't follow up on this the first time, but your formatting of the export list - and the excess whitespace in general - was seriously messed up.) -- gwern