Merging branch of my PR

Stream: new members

[Sebastian Monnet]

Apologies for what I'm sure is a very stupid question. @Yaël Dillies made a branch of my PR containing many improvements, and I would like to merge their branch into my PR, but I'm not sure how to.. could someone please advise me on this?

If I compare the branch to my PR (https://github.com/leanprover-community/mathlib/compare/alg_hom_of_ultrafilter...alg_hom_of_ultrafilter_golf), it says "These branches can be merged automatically", but I don't see a way to make that automatic merging happen. I have searched for the new branch in VSCode, but it claims that it doesn't exist

[Johan Commelin]

Does git pull help to make it show up in VScode?

[Johan Commelin]

Otherwise, you can do git merge some_other_branch on the command line (while you are on your own branch)

[Sebastian Monnet]

Johan Commelin said:

Does git pull help to make it show up in VScode?

Yes, that worked! Thank you so much

[Arthur Paulino]

When I want to download a particular branch I do git fetch origin branch-name