New CI labels. (#3736)

This PR adds two new labels to interact with CI systems:
* `CI: Keep up to date` tells mergify bot to auto-update the PR against develop but do not merge it. 
* `CI: No changelog needed` is meant to replace old `[ci no changelog needed]`
* `CI: Clean build required` marks PR as being incompatible with main development branch and will ensure that runners are cleaned before and after running jobs related to this PR.

Note that currently only first label is supported, others will follow with the build script update. However they need to be merged before, so I am able to develop and test them.

.github/mergify.yml

@@ -16,6 +16,8 @@ pull_request_rules:
           {%- endif -%}
   - name: Automatic PR update
     conditions:
-      - "label=CI: Ready to merge"
+      - or:
+          - "label=CI: Keep up to date"
+          - "label=CI: Ready to merge"
     actions:
       update:

.github/settings.yml

@@ -86,6 +86,15 @@ labels:
   - name: "CI: Ready to merge"
     color: "#ffffff"
     description: This PR is eligible for automatic merge
+  - name: "CI: Keep up to date"
+    color: "#ffffff"
+    description: Automatically update this PR to the latest develop.
+  - name: "CI: No changelog needed"
+    color: "#ffffff"
+    description: Do not require a changelog entry for this PR.
+  - name: "CI: Clean build required"
+    color: "#ffffff"
+    description: CI runners will be cleaned before and after this PR is built.
 
   - name: "Difficulty: Beginner"
     color: "#d1e9c4"