domain labels for already accepted MRs are still useful

In the case of short-circuited MRs (skipping the review process),
a MR can be closed before the CI job for assigning the Gitlab labels
is run. In this case, domain labels should still be assigned to
facilitate future searches for MRs by domain. Review labels are still
added in case a post-facto review is desired.


Former-commit-id: 7b12fb51

CI/handle_new_mr.py

@@ -120,7 +120,7 @@ def handle_new_merge_request(args):
         logging.critical("error communication with Gitlab API '%s'" % (e.error_message))
         sys.exit(1)
 
-    if not mr.state in ["opened","reopened"]:
+    if not mr.state in ["opened","reopened","merged"]:
         logging.debug("ignore merge request in '%s' state" % mr.state)
         sys.exit(0)