Whitespace changes.

(I had "git diff" set up to ignore whitespace changes, to I did not
notice that I pushed a commit with the code indented in this funky
way.)