Skip to content

Commit 9538b8a

Browse files
authored
Remove workaround for lean-update action (#196)
1 parent ddd3ae4 commit 9538b8a

File tree

1 file changed

+2
-3
lines changed

1 file changed

+2
-3
lines changed

.github/workflows/update.yml

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -18,11 +18,10 @@ jobs:
1818
uses: actions/checkout@v4
1919
- name: Get latest Lean nightly
2020
run: curl -s release.lean-lang.org | jq -r '.nightly[0].name' | sed 's/^/leanprover\/lean4:/' > lean-toolchain
21-
- name: Append empty lines to lake-manifest.json to trick lean-update into leaving the lean-toolchain file alone
22-
run: printf '\n%.0s' {1..10} >> lake-manifest.json
2321
- name: Update Lean project
2422
uses: leanprover-community/lean-update@main
2523
with:
2624
update_if_modified: lean-toolchain
2725
on_update_succeeds: "commit"
28-
on_update_fails: "issue"
26+
on_update_fails: "issue"
27+
update_lean_toolchain: "never"

0 commit comments

Comments
 (0)