0.3.1: Pull Requests
Learning Objectives
Pull requests are requests to merge, aka "pull" changes from 1 branch to another. They are typically used for code review before merging feature branches to the
mainbranch.Know how to create pull requests in GitHub
Know how to leave comments on and merge pull requests in GitHub
Introduction
A GitHub pull request (PR) is a request to merge or "pull" changes from 1 branch on GitHub to another. PRs are most commonly used for code review, where SWEs share PRs for peer review before merging that code to a main branch. Reviewers can comment on individual lines in the PR and request changes before the code is merged. Rocket uses PRs for student code submission and review.
How to create, comment on and merge pull requests
Below is a demo video for how to create, comment on and merge pull requests.
To create a pull request to merge a change from a feature branch to main (or any other branch), first push the latest changes from that feature branch from our local repo to GitHub.
Once the latest changes on that feature branch are in GitHub, we can navigate to the "Pull requests" tab in our repo's GitHub page and click "New pull request".
Verify we are merging the correct source and target branch, and correct commits and code changes. Once verified, click "Create pull request".
Leave a descriptive title and description for reviewers, then click "Create pull request".
If you are a reviewer or want to leave comments for your reviewer, hover over the relevant line of code and click the "+" icon to leave a comment on that line. To comment on multiple lines, click and drag the "+" icon over the relevant lines.
Once reviewers have approved the PR, click "Merge pull request" in the PR's Conversation tab to merge the relevant branches and close the PR.
After merging the PR, we should see the merged code in the target branch, in this case main.
Last updated
