You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository was archived by the owner on Nov 28, 2024. It is now read-only.
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: