From d473e4f458fc9cb8c603ccf4d54daeefbd8cea1b Mon Sep 17 00:00:00 2001
From: Ulli Hafner <ullrich.hafner@gmail.com>
Date: Fri, 1 Dec 2023 18:35:46 +0100
Subject: [PATCH] Use latest autograding.

---
 .github/workflows/autograding.yml | 2 +-
 .github/workflows/reporting.yml   | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/autograding.yml b/.github/workflows/autograding.yml
index db8e820e..307d71a3 100644
--- a/.github/workflows/autograding.yml
+++ b/.github/workflows/autograding.yml
@@ -26,7 +26,7 @@ jobs:
         env:
           BROWSER: chrome-container
         run: mvn -V --color always -ntp clean verify --file pom.xml '-Djenkins.test.timeout=5000' '-Dgpg.skip' -Ppit | tee maven.log
-      - name: Extract pull request number
+      - name: 'Extract pull request number'
         uses: jwalton/gh-find-current-pr@v1
         id: pr
       - name: Run Autograding
diff --git a/.github/workflows/reporting.yml b/.github/workflows/reporting.yml
index e3b40ad7..ea0ed742 100644
--- a/.github/workflows/reporting.yml
+++ b/.github/workflows/reporting.yml
@@ -150,14 +150,14 @@ jobs:
           status: ${{ steps.metrics.outputs.warnings }}
           color: 'orange'
           path: badges/warnings.svg
-      - name: Commit badge
+      - name: Commit updated badges
         continue-on-error: true
         run: |
           git config --local user.email "action@github.com"
           git config --local user.name "GitHub Action"
           git add badges/*.svg
           git commit -m "Update badges with results from latest autograding"
-      - name: Push badge commit
+      - name: Push updated badges to GitHub repository
         uses: ad-m/github-push-action@master
         if: ${{ success() }}
         with: