PR Merging Workflow
#
Implementation Review Criteria- Adheres to our conventions or can be patched up easily after merging, follows proper code style.
- Are there any implementation details that could be done better through alternate technologies/technical approaches?
- Does not touch any lines outside of the intended changes, eg through formatting or compilation.
- If the changes are to code intended as a public API, has a proper doc block been included?
#
Merge Time!If all of the checks in the template are met, any core developer may merge this PR. If the PR is authored by a core developer, they should probably be the ones to merge it.
Merging:
- GitHub offers several ways to merge a PR. Choose between the following strategies:
- Merge when the PR branch consists of atomic, well-described commits that are nice to have in the version history.
- Squash when lots of cleanup commits have accumulated. Please make sure to write a good commit message for the squash commit.
- GitHub offers several ways to merge a PR. Choose between the following strategies:
After merging:
- Make sure the issue (if none exists, the PR - but not both) belongs to the appropriate milestone. PRs in extensions cannot be assigned to core milestones, so assign it to the current release's project board instead.
- Close all relevant issues (if they are closed completely).
- Check for follow-up tasks:
- Merge related PRs (language files, extensions, documentations)
- Documentation updates
- Create issues for further follow-up tasks, if necessary.