Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

fix: docstring in Attributes.lean #4238

Merged
merged 3 commits into from
May 23, 2024
Merged

fix: docstring in Attributes.lean #4238

merged 3 commits into from
May 23, 2024

Conversation

meow-sister
Copy link
Contributor

Changing document string in Attributes.lean, in order to consistent with code in Lean.Parser.Attr.

@meow-sister meow-sister changed the title Update Attributes.lean fix: Fixing docstring in Attributes.lean. May 21, 2024
@meow-sister meow-sister changed the title fix: Fixing docstring in Attributes.lean. fix: Fixing docstring in Attributes.lean May 21, 2024
@semorrison semorrison added the awaiting-author Waiting for PR author to address issues label May 21, 2024
@meow-sister
fix: Fixing docstring in Attributes.lean
fad7ae4 
Changing document string in `Attributes.lean`, in order to consistent with code in `Lean.Parser.Attr`.
@leodemoura leodemoura changed the title fix: Fixing docstring in Attributes.lean fix: docstring in Attributes.lean May 21, 2024
@semorrison semorrison added awaiting-review Waiting for someone to review the PR and removed awaiting-author Waiting for PR author to address issues awaiting-review Waiting for someone to review the PR labels May 23, 2024
@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 May 23, 2024
@leanprover-community-mathlib4-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 097a4d5b6bc6b676e5bc20e58d77413c9a8ad6fd --onto ff37e5d512efcd3981290270a2fc3ecb100bbd0c. (2024-05-23 09:55:53)

@semorrison semorrison added this pull request to the merge queue May 23, 2024
Merged via the queue into leanprover:master with commit 258cc28 May 23, 2024
16 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@semorrison semorrison Awaiting requested review from semorrison

Assignees
No one assigned
Labels
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@meow-sister @leanprover-community-mathlib4-bot @semorrison