CI: Run coverage job on 'pr: dev-coverage' label in PRs (#6527)

This commit is contained in:
Geza Lore
2025-10-07 17:03:13 +01:00
committed by GitHub
parent 888169571b
commit 97707bdc72
3 changed files with 98 additions and 29 deletions
+1 -2
View File
@@ -159,8 +159,7 @@ CONTENTS_TEMPLATE
INDEX_TEMPLATE
# Report size
${COVERAGE_ROOT}
du -shc *
du -shc ${COVERAGE_ROOT}/*
# Set output
echo "coverage-pr-run-ids=${PR_RUN_IDS}" >> $GITHUB_OUTPUT