File tree Expand file tree Collapse file tree 1 file changed +0
-15
lines changed Expand file tree Collapse file tree 1 file changed +0
-15
lines changed Original file line number Diff line number Diff line change @@ -188,21 +188,6 @@ jobs:
188
188
run : |
189
189
build/stage1/bin/lean --stats src/Lean.lean
190
190
if : ${{ !matrix.cross }}
191
- - name : Test
192
- id : test
193
- run : |
194
- ulimit -c unlimited # coredumps
195
- time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/stage1 -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }}
196
- if : (matrix.wasm || !matrix.cross) && (inputs.check-level >= 1 || matrix.name == 'Linux release')
197
- - name : Test Summary
198
- uses : test-summary/action@v2
199
- with :
200
- paths : build/stage1/test-results.xml
201
- # prefix `if` above with `always` so it's run even if tests failed
202
- if : always() && steps.test.conclusion != 'skipped'
203
- - name : Check Test Binary
204
- run : ${{ matrix.binary-check }} tests/compiler/534.lean.out
205
- if : (!matrix.cross) && steps.test.conclusion != 'skipped'
206
191
- name : Build Stage 2
207
192
run : |
208
193
make -C build -j$NPROC stage2
You can’t perform that action at this time.
0 commit comments