Remove a stray ; that snuck into the middle of a comment.