.github: also run when PR is merged

https://stackoverflow.com/a/61565445/1708249
2026-07-30 12:33:02 +02:00 · 2023-05-30 09:00:59 +02:00
parent 8ffe839a99
commit 4ad676bb4e
1 changed files with 3 additions and 1 deletions
@@ -9,7 +9,9 @@ name: Bob the Builder
 #      - '*'
 on:
  pull_request_review:
-    types: [submitted]
+    types:
+      - submitted
+      - closed
  workflow_dispatch:

 jobs: