From 2e160291088ea90df4a9cb83ed539d6cb70d9019 Mon Sep 17 00:00:00 2001
From: Pedro Algarvio <pedro@algarvio.me>
Date: Wed, 10 Apr 2024 10:39:26 +0100
Subject: [PATCH] Select all available OS'es if `test:coverage` label is set

---
 tools/ci.py | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/tools/ci.py b/tools/ci.py
index 7bdbc588fda..12524435ce4 100644
--- a/tools/ci.py
+++ b/tools/ci.py
@@ -932,6 +932,7 @@ def get_pr_test_labels(
     """
     Set the pull-request labels.
     """
+    github_step_summary = os.environ.get("GITHUB_STEP_SUMMARY")
     gh_event_path = os.environ.get("GITHUB_EVENT_PATH") or None
     if gh_event_path is None:
         labels = _get_pr_test_labels_from_api(ctx, repository, pr=pr)
@@ -983,6 +984,17 @@ def get_pr_test_labels(
     else:
         ctx.info(f"No test labels for pull-request #{pr} on {repository}")
 
+    if "test:coverage" in test_labels:
+        ctx.info(
+            "Selecting ALL available OS'es because the label 'test:coverage' is set."
+        )
+        selected.add("all")
+        if github_step_summary is not None:
+            with open(github_step_summary, "a", encoding="utf-8") as wfh:
+                wfh.write(
+                    "Selecting ALL available OS'es because the label `test:coverage` is set.\n"
+                )
+
     if "all" in selected:
         selected = select_all
         available.clear()