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

[Merged by Bors] - chore(scripts): update nolints.txt #8189

Closed
wants to merge 1 commit into from

Conversation

leanprover-community-bot
Copy link
Collaborator

I am happy to remove some nolints for you!

@leanprover-community-bot
Copy link
Collaborator Author

bors r+

bors bot pushed a commit that referenced this pull request Jul 4, 2021
I am happy to remove some nolints for you!
@bors
Copy link

bors bot commented Jul 4, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(scripts): update nolints.txt [Merged by Bors] - chore(scripts): update nolints.txt Jul 4, 2021
@bors bors bot closed this Jul 4, 2021
@bors bors bot deleted the nolints branch July 4, 2021 02:55
b-mehta pushed a commit that referenced this pull request Jul 6, 2021
I am happy to remove some nolints for you!
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant