Skip to content

chore: CI: avoid fetching full repo in PR Release#12309

Open
Kha wants to merge 1 commit intoleanprover:masterfrom
Kha:push-tzwmywnvuryk
Open

chore: CI: avoid fetching full repo in PR Release#12309
Kha wants to merge 1 commit intoleanprover:masterfrom
Kha:push-tzwmywnvuryk

Conversation

@Kha
Copy link
Member

@Kha Kha commented Feb 4, 2026

No description provided.

@Kha Kha requested a review from kim-em as a code owner February 4, 2026 13:01
@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 Feb 4, 2026
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.

1 participant