Minor English improvement in a comment.