Add merge_group event type to all PR CI jobs (#2820)

moveit · Apr 30, 2024 · 7d2ae82 · 7d2ae82
1 parent 0f24369
commit 7d2ae82
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 0 deletions.
diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml
@@ -6,6 +6,7 @@ name: CI
 on:
   workflow_dispatch:
   pull_request:
+  merge_group:
   push:
     branches:
       - main

diff --git a/.github/workflows/format.yaml b/.github/workflows/format.yaml
@@ -6,6 +6,7 @@ name: Formatting (pre-commit)
 on:
   workflow_dispatch:
   pull_request:
+  merge_group:
   push:
     branches:
       - main

diff --git a/.github/workflows/tutorial_docker.yaml b/.github/workflows/tutorial_docker.yaml
@@ -6,6 +6,7 @@ on:
     - cron:  '0 17 * * 6'
   workflow_dispatch:
   pull_request:
+  merge_group:
   push:
     branches:
       - main