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

Suppress warnings for incomplete uni-patterns and partial use of head #281

Merged
merged 1 commit into from
Jul 22, 2024

Conversation

sgraf812
Copy link
Collaborator

@sgraf812 sgraf812 commented Jun 23, 2024

All the incomplete matches are in fact safe. The warnings only add noise.

#247 is related, but a non-solution.

@sgraf812 sgraf812 force-pushed the wip/incomplete-uni-patterns branch from 9173db0 to 80244e0 Compare July 12, 2024 15:22
@sgraf812 sgraf812 changed the title Do not warn for incomplete uni-patterns Suppress warnings for incomplete uni-patterns and partial use of head Jul 12, 2024
@sgraf812 sgraf812 mentioned this pull request Jul 12, 2024
All the incomplete matches are in fact safe. The warnings only add
noise.
@sgraf812 sgraf812 force-pushed the wip/incomplete-uni-patterns branch from 80244e0 to 144fd44 Compare July 15, 2024 07:53
@sgraf812 sgraf812 merged commit 635cc81 into master Jul 22, 2024
26 checks passed
@andreasabel andreasabel deleted the wip/incomplete-uni-patterns branch July 22, 2024 17:08
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant