Skip to content

Conversation

@Kha
Copy link
Member

@Kha Kha commented Oct 16, 2025

No description provided.

@Kha
Copy link
Member Author

Kha commented Oct 16, 2025

My previous testing seems to have worked only accidentally because I must have been testing it in the root dir itself, but this appears to be working from within any workspace folder

@Kha Kha force-pushed the push-msnornyvwmwn branch from 4baa2fa to 167260f Compare October 16, 2025 08:43
@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 Oct 16, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 114f7e42f1abd10885e91698cd2910b1e4d76083 --onto 14ff08db6f651775ead432d367b6b083878bb0f9. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-16 09:52:40)

@leanprover-bot
Copy link
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 114f7e42f1abd10885e91698cd2910b1e4d76083 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-16 09:52:42)

@Kha Kha added this pull request to the merge queue Oct 16, 2025
Merged via the queue into leanprover:master with commit 5c7b003 Oct 16, 2025
16 checks passed
@Kha Kha deleted the push-msnornyvwmwn branch October 16, 2025 20:51
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

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.

3 participants