This seems to be a redundant line.  It's a very minor correction, but I thought it better to drop it on the mailing list rather than letting it get lost.

Jesse Weinstein