Skip to content

fix: lake: moduleCodegen test on Windows - #15220

Merged
tydeu merged 1 commit into
leanprover:masterfrom
tydeu:lake/fix-moduleCodgen
Sep 18, 2026
Merged

tydeu merged 1 commit into
leanprover:masterfrom
tydeu:lake/fix-moduleCodgen

Conversation

@tydeu

@tydeu tydeu commented Sep 18, 2026

Copy link
Copy Markdown
Member

This PR fixes the moduleCodegen test on Windows, which was broken due to testing for Unix paths.

@tydeu tydeu added release-ci Enable all CI checks for a PR, like is done for releases changelog-no Do not include this PR in the release changelog labels Sep 18, 2026
@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Sep 18, 2026
@tydeu
tydeu marked this pull request as ready for review September 18, 2026 19:36
@tydeu
tydeu added this pull request to the merge queue Sep 18, 2026
Merged via the queue into leanprover:master with commit 6d7e348 Sep 18, 2026
39 of 43 checks passed
@tydeu
tydeu deleted the lake/fix-moduleCodgen branch September 19, 2026 02:35
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-no Do not include this PR in the release changelog release-ci Enable all CI checks for a PR, like is done for releases toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant