chore: give the 'post or update summary comment' job a descriptive na…

…me (#19382) It can be useful to have a useful *job* (and not *workflow step*) name, e.g. in case one looks at JSON information in the queueboard data, about failed CI.
leanprover-community · Nov 22, 2024 · 65cc629 · 65cc629
1 parent 9e7e427
commit 65cc629
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/.github/workflows/PR_summary.yml b/.github/workflows/PR_summary.yml
@@ -5,6 +5,7 @@ on:
 
 jobs:
   build:
+    name: "post-or-update-summary-comment"
     runs-on: ubuntu-latest
 
     steps: