Skip to content

ci: add actionable fix command to toolchain consistency check#825

Open
kim-em wants to merge 1 commit intomainfrom
ci-actionable-toolchain-fix
Open

ci: add actionable fix command to toolchain consistency check#825
kim-em wants to merge 1 commit intomainfrom
ci-actionable-toolchain-fix

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Apr 8, 2026

This PR adds a "To fix, run:" suggestion to the lean-toolchain consistency check, showing the exact cp commands needed to update mismatched test project toolchains.

🤖 Prepared with Claude Code

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@github-actions
Copy link
Copy Markdown
Contributor

github-actions bot commented Apr 8, 2026

Preview for this PR is ready! 🎉

@david-christiansen
Copy link
Copy Markdown
Collaborator

I think this might be nicer as a GH action? So we could run:

!consistent

and then it would fix all consistency issues in the obvious way and push a commit to the PR?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants