chore: fix test exclusion (#5990)

You cannot pass `-E` to `ctest` multiple times
leanprover · Nov 7, 2024 · 5f7a40a · 5f7a40a
1 parent 70435df
commit 5f7a40a
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 1 deletion.
diff --git 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
@@ -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";