ci: ensure PR titles are no longer than 72 characters (#3267)

GitHub wraps the titles of commits if they are longer than 72 characters. See fbd4192e2a for example.

There is a convention that titles should be no more than 50 characters: https://cbea.ms/git-commit/#limit-50
This however makes crafting the message quite difficult, esp. with our use of conventional commit messages, thus limiting it to 72 seems more reasonable as that is where tooling (.e.g GitHub) seems to "break".

.github/workflows/ci.yml

@@ -300,4 +300,14 @@ jobs:
             test
             ci
             refactor
-          requireScope: false
+          require_scope: false
+
+      - name: Check PR title length
+        run: |
+          title="${{ github.event.pull_request.title }}"
+          title_length=${#title}
+          if [ $title_length -gt 72 ]
+          then
+            echo "PR title is too long (greater than 72 characters)"
+            exit 1
+          fi