Allow source branch to be deleted from Closed Merge Request
Description
In our use of gitlab, it is practise that when a merge request gets closed without merging, that's usually because a bug has been fixed differently in another branch&merge request. In these cases we want to delete these unmerged branches, not to pile up too much old, unmaintained, generally useless branches, clogging the list of branches. And only actively developed branches, or branches for merge requests that just cannot get merged "now" (for whatever procedural reasons) are kept in the main repository.
After merging a merge request, one has a "Remove Source Branch" button on the merge request page, and one can also tick the checkbox to do so even before hitting merge.
Yet, such a "reminder" does not exist for closing merge requests and users keep forgetting that this needs to be done on top of closing a merge request.
Proposal
On the page of a closed merge request, there should be a 'remove source branch' button, just like on the page of a merged request.
Links / references
just one example
https://gitlab.cern.ch/lhcb/Rec/merge_requests/872#note_862791
In fact the one who forgot to delete the branch in this example usually needs to remind me to do so.