[mirashii]

Pulled in this context means pulled into the tree, not removed as the common parlance might indicate, for those who were a bit confused like myself.

[klez]

Wouldn't the correct (or, at least, less confusing) term then be "merged" if that's the case?

[sokoloff]

"pull" is a git command to merge and update

https://git-scm.com/docs/git-pull

[gnulinux]

Pull is also correct. Somehow merge is a little more popular but pull is certainly correct too. Remember the word "Pull Request".

[angelsl]

My bad, should've said merged.

I wrote the comment immediately after reading Linus's email.