chore: make PR title check work as a merge_group check (#2987)

.github/workflows/pr-title.yml

@@ -1,8 +1,9 @@
 name: Check PR title for commit convention
 
 on:
+  merge_group:
   pull_request:
-    types: [opened, edited]
+    types: [opened, synchronize, reopened, edited]
 
 jobs:
   check-pr-title:
@@ -12,6 +13,8 @@ jobs:
         uses: actions/github-script@v6
         with:
           script: |
-            if (!/^(feat|fix|doc|style|refactor|test|chore|perf): .*[^.]($|\n\n)/.test(context.payload.pull_request.title)) {
+            const msg = context.payload.pull_request? context.payload.pull_request.title : context.payload.merge_group.head_commit.message;
+            console.log(`Message: ${msg}`)
+            if (!/^(feat|fix|doc|style|refactor|test|chore|perf): .*[^.]($|\n\n)/.test(msg)) {
               core.setFailed('PR title does not follow the Commit Convention (https://leanprover.github.io/lean4/doc/dev/commit_convention.html).');
             }