Skip to content

Conversation

@zhangwen0411
Copy link

No description provided.

@sohah
Copy link

sohah commented Jun 23, 2024

@yannicnoller , this is not a useful change. I think we can close this PR.

@yannicnoller
Copy link
Member

@sohah do you think the "!*" is a typo in the original code? From looking at it, I think I agree that we should change it.

@sohah
Copy link

sohah commented Jul 15, 2024

@yannicnoller , yeah, sure it's a valid typeo fix, I meant, the PR is not fixing any unsound behavior. But, of course, let's accept this change then.

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.

3 participants