cosmetics

.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