Merge pull request #300 from mtzguido/ciqueue

ci: try out merge queue
FStarLang · Jan 8, 2025 · 1f7f57c · 1f7f57c
2 parents 985749f + 6f38b03
commit 1f7f57c
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -4,6 +4,7 @@ on:
     branches-ignore:
     - _**
   pull_request:
+  merge_group:
   workflow_dispatch:
 
 defaults: