From 1e2d1afc049222ecd4588e68ec370007b4020472 Mon Sep 17 00:00:00 2001
From: Matthias Frei <matzf@scion.org>
Date: Mon, 15 Jul 2024 13:53:15 +0200
Subject: [PATCH] cosmetics

---
 .github/workflows/pr-title.yml | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

diff --git a/.github/workflows/pr-title.yml b/.github/workflows/pr-title.yml
index c494c14a49..0747e19065 100644
--- a/.github/workflows/pr-title.yml
+++ b/.github/workflows/pr-title.yml
@@ -2,31 +2,29 @@ name: Check the pull request title
 
 on:
   pull_request:
-    types: [opened, edited, reopened]
+    types: [opened, edited, reopened, synchronize]
 
 jobs:
-  setup-and-test:
+  check:
     runs-on: ubuntu-latest
     steps:
     - name : Check the PR title
       env:
         TITLE: ${{ github.event.pull_request.title }}
       run: |
+        echo "Check that PR is of the form `<subystem>: <lowercase message>` :monocle_face:" >> $GITHUB_STEP_SUMMARY
         url='https://docs.scion.org/en/latest/dev/git.html#good-commit-messages'
         if [[ ! "$TITLE" =~ ^[a-z0-9,/]*:[[:space:]] ]]; then
-          echo "The PR title should start with \"<substystem>: \"."
-          echo "See $url"
+          echo "::warning {The PR title should start with `<substystem>: `.\nSee $url}"
           exit 1
         fi
         # Title should be lower case; initialisms and identifiers still occur occasionally and should be allowed.
         # -> enforce only the first word
         if [[ ! "$TITLE" =~ ^[a-z0-9,/]*:[[:space:]][a-z] ]]; then
-          echo "The PR title should be lower case. (Enforced on first letter)"
-          echo "See $url"
+          echo "::warning {The PR title should be lower case. (Enforced on first letter)\nSee $url}"
           exit 1
         fi
         if [[ $TITLE =~ \.[[:space:]]*$ ]]; then
-          echo "The PR title should not end with a \".\""
-          echo "See $url"
+          echo "::warning {The PR title should not end with a \".\".\nSee $url}"
           exit 1
         fi