Fix a typo in a comment used for documentation. No code changes.