Add label to pull requests that were merged

[mschoettle]

Due to a limitation on GitHub's pull request API it is not possible to mark a PR as merged. It would be good to add at least a label to the merged ones (that were merged on GitLab) to distinguish them from closed MRs/PRs.

[spruce]

Sounds good. I just don't have the time to add it currently. I would be willing to accept a PR for this feature.