Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Closed PR was merged #154

Open
figadore opened this issue May 5, 2022 · 0 comments
Open

Closed PR was merged #154

figadore opened this issue May 5, 2022 · 0 comments
Labels
bug GitHub :octocat: Github-specific issue good first issue help wanted

Comments

@figadore
Copy link

figadore commented May 5, 2022

After running mp push, a PR was supposed to be excluded from the batch updates was closed in the GitHub UI. Then mp merge was run. The closed PR was merged anyway. This seems like undesirable behavior.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug GitHub :octocat: Github-specific issue good first issue help wanted
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@figadore @jakegut