Skip to content

Commit 1d91c3f

Browse files
authored
ci: set TEST_ARGS manually (#422)
Pending leanprover/lean-action#153, manually set `TEST_ARGS`. As can be seen from the CI runs, this now correctly results in running `lake test --wfail --iofail`.
1 parent 4f3737a commit 1d91c3f

1 file changed

Lines changed: 4 additions & 0 deletions

File tree

.github/workflows/lean_action_ci.yml

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,10 @@ jobs:
1414
runs-on: ubuntu-latest
1515
steps:
1616
- uses: actions/checkout@v4
17+
- name: Set TEST_ARGS manually
18+
run: |
19+
echo "TEST_ARGS='--wfail --iofail'" >> $GITHUB_ENV
20+
shell: bash
1721
- uses: leanprover/lean-action@v1
1822
with:
1923
build-args: "--wfail --iofail"

0 commit comments

Comments
 (0)