Comment 5 for bug 1291537

Jason: Either of your options sounds fine to me; if you think there's a chance that someone else will wander down the same road then the "fix the whitespace" option might be best!