* Add checkbox to delete pull branch after successful merge
* Omit DeleteBranchAfterMerge field in json
* Log a warning instead of error when PR head branch deleted
* Add DefaultDeleteBranchAfterMerge to PullRequestConfig
* Add support for delete_branch_after_merge via API
* Fix for API: the branch should be deleted from the HEAD repo
If head and base repo are the same, reuse the already opened ctx.Repo.GitRepo
* Don't delegate to CleanupBranch, only reuse branch deletion code
CleanupBranch contains too much logic that has already been performed by the Merge
* Reuse gitrepo in MergePullRequest
Co-authored-by: Andrew Thornton <art27@cantab.net>
78118a3b02