Skip to content

Actually *register* the lint groups#106

Merged
BD103 merged 4 commits intomainfrom
groups-fix
Sep 25, 2024
Merged

Actually *register* the lint groups#106
BD103 merged 4 commits intomainfrom
groups-fix

Conversation

@BD103
Copy link
Copy Markdown
Member

@BD103 BD103 commented Sep 25, 2024

Looks like I forgot to register the lint groups introduced in #98. Whoops!

While I'm at it, I also changed the visibility of some items so that less is public that before.

@BD103 BD103 added A-Linter Related to the linter and custom lints C-Bug A bug in the program labels Sep 25, 2024
@BD103 BD103 changed the title Actually _register_ the lint groups Actually *register* the lint groups Sep 25, 2024
@BD103 BD103 marked this pull request as ready for review September 25, 2024 01:31
Copy link
Copy Markdown
Collaborator

@bas-ie bas-ie left a comment

Choose a reason for hiding this comment

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

Ah, makes sense!

@BD103 BD103 merged commit 1dd2304 into main Sep 25, 2024
@BD103 BD103 deleted the groups-fix branch September 25, 2024 01:56
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

A-Linter Related to the linter and custom lints C-Bug A bug in the program

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants