Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - chore(data/countable/defs): add explanation of nolint#17732

Closed
kim-em wants to merge 2 commits intomasterfrom
Prop_countable
Closed

[Merged by Bors] - chore(data/countable/defs): add explanation of nolint#17732
kim-em wants to merge 2 commits intomasterfrom
Prop_countable

Conversation

@kim-em
Copy link
Copy Markdown
Collaborator

@kim-em kim-em commented Nov 27, 2022


Open in Gitpod

@kim-em kim-em added the awaiting-CI The author would like to see what CI has to say before doing more work. label Nov 27, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Nov 27, 2022
@kim-em kim-em changed the title chore(data/countable/defs): remove nolint chore(data/countable/defs): add explanation of nolint Nov 27, 2022
@kim-em kim-em added easy < 20s of review time. See the lifecycle page for guidelines. awaiting-review The author would like community review of the PR docs This PR is about documentation labels Nov 27, 2022
@riccardobrasca
Copy link
Copy Markdown
Member

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Dec 1, 2022
bors bot pushed a commit that referenced this pull request Dec 1, 2022


Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Dec 1, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(data/countable/defs): add explanation of nolint [Merged by Bors] - chore(data/countable/defs): add explanation of nolint Dec 1, 2022
@bors bors bot closed this Dec 1, 2022
@bors bors bot deleted the Prop_countable branch December 1, 2022 13:29
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

docs This PR is about documentation easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants