From 8cdf7284f857e1e0a2d5f0c7289ca8bdd233938d Mon Sep 17 00:00:00 2001
From: Pieter Noordhuis <pieter.noordhuis@databricks.com>
Date: Wed, 26 Jul 2023 14:48:05 +0200
Subject: [PATCH] Add merge_group trigger for build (#612)

## Changes

Also see [GitHub
docs](https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/configuring-pull-request-merges/managing-a-merge-queue#triggering-merge-group-checks-with-github-actions).

## Tests

n/a
---
 .github/workflows/push.yml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 0f9b601616..1dcf3eaf30 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -5,6 +5,8 @@ on:
     types: [opened, synchronize]
   push:
     branches: [main]
+  merge_group:
+    types: [checks_requested]
 
 jobs:
   tests: