Skip to content

Comments

feat: add #guard_msgs configuration syntax and update documentation#3892

Closed
kmill wants to merge 1 commit intoleanprover:masterfrom
kmill:guardmsgs_cmd_syntax
Closed

feat: add #guard_msgs configuration syntax and update documentation#3892
kmill wants to merge 1 commit intoleanprover:masterfrom
kmill:guardmsgs_cmd_syntax

Conversation

@kmill
Copy link
Collaborator

@kmill kmill commented Apr 12, 2024

Implementation for this configuration syntax will appear after a stage0 update.

Implementation for this configuration syntax will appear after a stage0 update.
@kmill
Copy link
Collaborator Author

kmill commented Apr 12, 2024

(@digama0 If this looks good, feel free to test out putting it on the merge queue.)

@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 Apr 12, 2024
@digama0
Copy link
Collaborator

digama0 commented Apr 12, 2024

LGTM but it's failing.

@kmill
Copy link
Collaborator Author

kmill commented Apr 12, 2024

I think I figured out the staging issues here, and should be doable with a single merge in #3883. Just waiting on verifying it passes the tests.

@kmill kmill closed this Apr 12, 2024
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.

2 participants