Zulip Chat Archive

Stream: new members

Topic: Merging branch of my PR


Sebastian Monnet (Apr 27 2022 at 13:47):

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 (Apr 27 2022 at 13:48):

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

Johan Commelin (Apr 27 2022 at 13:49):

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

Sebastian Monnet (Apr 27 2022 at 13:53):

Johan Commelin said:

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

Yes, that worked! Thank you so much

Arthur Paulino (Apr 27 2022 at 14:00):

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


Last updated: Dec 20 2023 at 11:08 UTC