Merge requests aren't removing source branches
Even though our developers are selecting the checkbox to delete the source branch when merging a Merge Request, the source branch doesn't get deleted.
Upon merging, we see "The changes were merged into 'develop' with 'a0b1c2d3' - The source branch is being removed".
A minute or so later, the change pages to say "The changes were merged into 'develop' with 'a0b1c2d3' - You can remove source branch now".
We're using Enterprise Edition 10.8.4-ee gitlab-ce@f80a52846a4abbb4abdd42cd9736dcbc2a34840a. Is this a known problem? If not, how can I get more information that might be helpful?