Topic: Hint about merging
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.
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
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.
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?
Yury G. Kudryashov (Mar 31 2021 at 21:30):
Feel free to pr!
Last updated: May 12 2021 at 22:15 UTC