File tree Expand file tree Collapse file tree 1 file changed +4
-4
lines changed Expand file tree Collapse file tree 1 file changed +4
-4
lines changed Original file line number Diff line number Diff line change @@ -109,7 +109,7 @@ jobs:
109109 # re-running a run does not update that list, and we do want to be able to
110110 # rerun the workflow run after setting the `release-ci`/`merge-ci` labels.
111111 run : |
112- check_level=0
112+ check_level=1
113113
114114 if [[ -n "${{ steps.set-nightly.outputs.nightly }}" || -n "${{ steps.set-release.outputs.RELEASE_TAG }}" ]]; then
115115 check_level=2
@@ -137,7 +137,7 @@ jobs:
137137 console.log(`level: ${level}`);
138138 // use large runners where available (original repo)
139139 let large = ${{ github.repository == 'leanprover/lean4' }};
140- const isPr = "${{ github.event_name }}" == "pull_request ";
140+ const isMerge = "${{ github.event_name }}" == "merge_group ";
141141 let matrix = [
142142 /* TODO: to be updated to new LLVM
143143 {
@@ -229,8 +229,8 @@ jobs:
229229 // 2. To skip it in merge queues as it takes longer than the Linux build and adds
230230 // little value in the merge queue
231231 // 3. To run it in release (obviously)
232- "check-level": isPr ? 0 : 2,
233- "secondary": isPr ,
232+ "check-level": isMerge ? 0 : 2,
233+ "secondary": isMerge ,
234234 },
235235 {
236236 "name": "Windows",
You can’t perform that action at this time.
0 commit comments