Zulip Chat Archive

Stream: general

Topic: Hint about merging


view this post on Zulip Yury G. Kudryashov (Mar 31 2021 at 20:26):

I often find myself in the following situation:

  • I start branch A.
  • I decide that A is too large for 1 PR, so I cherry-pick some changes to another branch B, and start a separate PR.
  • Then I make changes to branch B (e.g., because of reviewers' comments).
  • Then branch B is merged into master, and I have conflicts in branch A.

I guess other people may have the same problem, so let me share my way of dealing with it without need to manually resolve conflicts.

  • Once I cherry-pick changes from A to B, I merge the new branch B to A (you can do it later with git merge sha1hash).
  • When B is merged to master, I do git checkout master && git pull && git checkout B && git merge master && git checkout A && git merge B. Often all merges happen without conflicts.

view this post on Zulip Eric Wieser (Mar 31 2021 at 20:35):

You can abbreviate that last command to

git fetch origin && git checkout B && git merge origin/master && git checkout A && git merge B

Which saves moving your working tree to master and back

view this post on Zulip Eric Wieser (Mar 31 2021 at 20:37):

But yes, the key trick is to merge bors' copy of your PR back into the branch it came from before merging that branch into follow-up PRs. The other trick is to run leanproject get-cache --rev origin/master immediately after that process, to start your cache rebuild somewhere reasonable.

view this post on Zulip Alex J. Best (Mar 31 2021 at 21:19):

Can we put these tips in the docs or somewhere less transient/easier to find than zulip?

view this post on Zulip Yury G. Kudryashov (Mar 31 2021 at 21:30):

Feel free to pr!


Last updated: May 12 2021 at 22:15 UTC