This repository was archived by the owner on Nov 28, 2024. It is now read-only.

Description
Once the pull request is reviewed and approved, our workflow is that the author should merge it. This can be done easily through GitHub UI (there is a "Squash and merge" button).
There are a couple of problems with this:
- We can't do it through command line.
- After it's done, the local branch becomes useless. Sometimes people will accidentally continue working in there, thinking it's nw at
origin/master which is not the case.
Ideally, we want a command git pull-request --merge which will:
- Merge into
origin/master.
- Close pull request.
- Delete local branch.
What are your thoughts?