Skip to content

Commit 895e35a

Browse files
committed
chore: skip OS X aarch64 CI only in merge groups
1 parent 8807893 commit 895e35a

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

.github/workflows/ci.yml

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -138,6 +138,7 @@ jobs:
138138
// use large runners where available (original repo)
139139
let large = ${{ github.repository == 'leanprover/lean4' }};
140140
const isPr = "${{ github.event_name }}" == "pull_request";
141+
const isMerge = "${{ github.event_name }}" == "merge_group";
141142
let matrix = [
142143
/* TODO: to be updated to new LLVM
143144
{
@@ -229,7 +230,7 @@ jobs:
229230
// 2. To skip it in merge queues as it takes longer than the Linux build and adds
230231
// little value in the merge queue
231232
// 3. To run it in release (obviously)
232-
"check-level": isPr ? 0 : 2,
233+
"check-level": isMerge ? 2 : 0,
233234
"secondary": isPr,
234235
},
235236
{

0 commit comments

Comments
 (0)