ci: attribute co-authorship of a PR based on its commits

It often happens that multiple people contribute to a single PR. To correctly attribute authorship, GitHub supports the `Co-authored-by` convention. This line however needs to be at the very end of the commit message.

Because we are also automatically adding the pull-request number to the commit message, we cannot add these lines ourselves. Doing this manually is error-prone anyway so with this patch, we are extending the commit message template to automatically populate this from the commits within the pull request.

Pull-Request: #4069.

.github/mergify.yml

@@ -8,6 +8,13 @@ defaults:
         {{ body | get_section("## Description", "") }}
         
         Pull-Request: #{{ number }}.
+        {# Here comes some fancy Jinja2 stuff for correctly attributing co-authorship: #}
+        {% for commit in (commits | unique(False, 'email_author')) | rejectattr("author", "==", author) %}
+          {% if commit.parents|length == 1 %}
+        Co-Authored-By: {{ commit.author }} <{{ commit.email_author }}>
+          {% endif %}
+        {% endfor %}
+        {# GitHub requires that the `Co-authored-by` lines are AT THE VERY END of a commit, hence nothing must come after this. #}
 
 pull_request_rules:
   - name: Ask to resolve conflict