Minor whitespace fix in a comment.