Skip to content

Moving description of ruler to Non-boolean settings in Usage.md - #141

Merged
joneugster merged 1 commit into
leanprover-community:mainfrom
jyoo980:update-docs
Aug 21, 2026
Merged

Moving description of ruler to Non-boolean settings in Usage.md#141
joneugster merged 1 commit into
leanprover-community:mainfrom
jyoo980:update-docs

Conversation

@jyoo980

@jyoo980 jyoo980 commented Aug 19, 2026

Copy link
Copy Markdown
Contributor

ruler was previously described as a setting with a Boolean value. It is a number not a boolean, and should be described under non-boolean settings.

@joneugster joneugster left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

@joneugster
joneugster merged commit c846aae into leanprover-community:main Aug 21, 2026
5 checks passed
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