To me it reads the same, only that "their" sounds a bit weird since it's usually used for multiple persons. I don't really care.

@brammool I'm just going to give you a heads up. People get really angry about this type of thing nowadays. Being as important of a project as this is, I definitely won't be the last person to make this PR.

Also, what's called "cancel culture" is something that's really out of hand these days. If you're a public figure and you do something that might appear sexist or racist to some people, those people will take it way out of proportion and it can have serious consequences. Richard Stallman just recently fell victim to this. He said some words that were not very sensitive, and someone saw them, got really angry, and wrote an article misquoting him. No one knew that the quote was wrong, and no one bothered to check, they all just took it for fact, and his life was turned upside down in an instant. By not changing this, you're putting yourself at risk of being labeled a "sexist" and/or a "misogynist" by the next person that comes along and sees that you didn't/won't change it.

I know this type of thing ("his" vs "their") isn't a big deal to you. And I will give you the benefit of the doubt (something people are really bad at doing nowadays from what I've seen) and assume you are not a sexist or misogynist, and that it really does read the same to you. But a growing number of people in the world don't feel that way. They feel that using "his" when you mean everyone makes woman feel left out. Women in programming is something a lot of people are advocating for right now, so using "his" like this would be a big no-no for them.

In English, "their" is an acceptable singular pronoun when you don't know the gender of the person. I recommend watching this short video.

So far I've tried to leave out my personal opinion from what I've said and just state what I see to be the facts about what people think and do nowadays, but I will include it here. Personally I don't go as crazy as some other people when it comes to this stuff. I'm currently in a programming related slack that has a bot that says something any time someone uses the word "guys" (as in, "what do you guys thing about ...") and I think that's too far. That being said, I do think that using "his" to mean everyone is not inclusive, and I don't think it should be used in spaces that are open to both men and women, such as programming.

This is not a useful discussion.

Just FYI: it has been included as of eab6dff