Closed PR was merged #154
Description
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.
{{ message }}