Git workflow

Merging version branch back into master

Let's say we made some fixes in version branch 0.42.x and we want to merge them back into master.

• Create branch chore-merge-0.42.x from master:

  git checkout master
  git pull
  git checkout -b chore-merge-0.42.x

• Merge feature branch into it: git merge 0.42.x
• Resolve any conflicts
• Push it: git push origin chore-merge-0.42.x
• Create a PR into master with a title like "Merge 0.42.x into master". In the description, list the PRs to 0.42.x that are merged: "Merges #4249, #4250"