merge or rebase when updating non-master branch of mathlib?

Stream: new members

[Shanghe Chen]

Hi what is the recommended work flow for updating non master branch of mathlib with newest master commit? Personally I prefer rebasing my developing branch on master, but I am also afraid that it messes up for others pulling it.

[Kevin Buzzard]

I type git merge master in my branch and it works fine

[Eric Wieser]

There is little point in rebasing because we squash commits anyway when we merge

[Shanghe Chen]

Sure thanks! I will stick to merge rather than rebase too!

[Yaël Dillies]

I've personally recently switched to using rebase because it helps me stacking PRs on top of each other

[Eric Wieser]

I don't see why that helps any more than merging?

[Eric Wieser]

Whichever approach you choose, the key thing is to recover from the rebase that bors does

[Yaël Dillies]

Eric Wieser said:

I don't see why that helps any more than merging?

It lets me drop commits that correspond to dependency PRs that were merged

[Michael Rothgang]

I would say: either way is fine - use whichever you prefer. Merge can be easier; using rebase is useful for e.g. stacked PR. (mathlib squashes each PR before merging, so for each PR there is just one commit merged, containing all the changes. Other open source projects merge all commits separately; in that case, rebase makes the history of commits cleaner.)