If there are merge conflicts, it’s best to resolve them locally.
Check whether you need to make any Pro-specific adjustments to the code
Review and approve your changes
You usually do this yourself. In case you had to make non-trivial adjustments, it’s also okay to request a proper peer review.
Set the merge style to “Create a merge commit” (regular merge)
Do not use “Squash and merge”! If you accidentally squash, it’s not a disaster, but it will create a bit of noise on the subsequent PR from Community.
We want a regular merge to preserve the commit history from Community
Merge the PR
Note that Github remembers the merge style of your last PR in this repo, so for your next “regular” PR, you may have to manually set it to “Squash and merge” again.
I thought we could make our merge instructions for the Pro repo a little bit more actionable and self-documenting.
We can also set the
reviewers
field, to automatically assign the actor as reviewer. That way, the PR e.g. shows up in your “Requested Reviews” list.See below how the PR description would look.
Related #123
@jotaen4tinypilot, please merge your changes from the Community repository:
master
Note that Github remembers the merge style of your last PR in this repo, so for your next “regular” PR, you may have to manually set it to “Squash and merge” again.