From 5f7a40ae48ede0b9e15e7c24d2d59dd214175297 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 7 Nov 2024 11:41:47 +0100 Subject: [PATCH] chore: fix test exclusion (#5990) You cannot pass `-E` to `ctest` multiple times --- .github/workflows/ci.yml | 2 +- tests/lean/run/task_test_io.lean | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index db74ff2a7e5d..c94e76334064 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -419,7 +419,7 @@ jobs: if [[ '${{ matrix.name }}' == 'Linux Debug' ]]; then ulimit -s unlimited fi - time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/stage1 -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }} -E "leanruntest_task_test_io" + time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/stage1 -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }} if: (matrix.wasm || !matrix.cross) && needs.configure.outputs.check-level >= 1 - name: Test Summary uses: test-summary/action@v2 diff --git a/tests/lean/run/task_test_io.lean b/tests/lean/run/task_test_io.lean index de2ffb643999..f84492e35ce8 100644 --- a/tests/lean/run/task_test_io.lean +++ b/tests/lean/run/task_test_io.lean @@ -1,3 +1,5 @@ +#exit -- TODO + #eval id (α := IO _) do let t1 ← IO.asTask $ Nat.forM 10 fun _ => IO.println "hi"; let t2 ← IO.asTask $ Nat.forM 10 fun _ => IO.println "ho";