-
Type:
Bug
-
Status: Open
-
Priority:
Major
-
Resolution: Unresolved
-
Affects Version/s: 1.0.1
-
Fix Version/s: None
-
Component/s: Developer Tools
-
Labels:None
When using the merge script to merge PRs against non-master branches, the PR on Github doesn't get closed.