Synching Branch

Stream: mathlib4

[David Ledvinka]

If you are working on branch of mathlib (in particular one that is in an ongoing PR) whats the correct way to "update" the branch with the changes to master?

[Etienne Marion]

merge origin/master I think? At least that’s what I do.

[Yaël Dillies]

git fetch; git merge origin/master (on your branch) is the beginner-friendly option. More advanced options are git fetch; git rebase origin/master and similar (but I would advise you against them for now)

[Etienne Marion]

Oh I forgot git :sweat_smile: I have never understood what git fetch does though

[Yaël Dillies]

It simply instructs git to update its local knowledge of the remote

[Etienne Marion]

I see. I thought that merging an origin branch would automatically pick up the most recent version available online

[Yaël Dillies]

No, it merely picks up what your local git thinks origin/master is. It just happens that vscode comes with the good default option of running git fetch every five minutes or something like that

[Etienne Marion]

Oh I see, thanks!

[Junyan Xu]

It just happens that vscode comes with the good default option of running git fetch every five minutes or something like that

Doesn't appear so for me ... I always manually fetch before merging master, otherwise it could be days or months old ...

okay I found these settings

image.png

[Yury G. Kudryashov]

You can git pull from master instead of git merge

[Junyan Xu]

Seems I need git pull origin master --no-ff if there is a conflict, but indeed a shorter single command is nice!

[Yury G. Kudryashov]

Your editor probably has a plugin that hides all these commands behind a nice UI.

[Yury G. Kudryashov]

I know that VS Code and Emacs have git extensions. I guess, nvim has one too.