If the doc change is trivial, yes. If it's a significant change in the meaning of the text and how it relates to the code it accompanies, then it should be a separate pull request.
A good litmus test is, "Is there value to the community in having this as a separate pull request when someone is browsing the commit history?"
In other words, if this only matters to me and is part of my own crusade (but one that the larger community is likely to actively object to), then I should keep it to myself.
The change in question here could have been part of a larger commit of changes to documentation and comments, where the overwhelming majority of changes would be considered valuable by the majority of the community.
