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.

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

CodeQL: fix filter names #9

Merged
merged 1 commit into from
Dec 7, 2023
Merged

CodeQL: fix filter names #9

merged 1 commit into from
Dec 7, 2023

Conversation

pjonsson
Copy link
Owner

@pjonsson pjonsson commented Dec 7, 2023

Some warnings are in groups, and
some warnings are "top level". The
warnings that commit d27496d
tried to filter out are at the top
level, so update the names for that.

Some warnings are in groups, and
some warnings are "top level". The
warnings that commit d27496d
tried to filter out are at the top
level, so update the names for that.
@pjonsson pjonsson merged commit ae52e3a into develop Dec 7, 2023
0 of 23 checks passed
@pjonsson pjonsson deleted the codeql-filters branch December 9, 2023 10:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
1 participant