Open zhangwen0411 opened 1 year ago
@yannicnoller , I do not think this is a useful change. The message itself had not changed, so I am not sure what difference this PR would introduce. I suggest we close this PR.
@sohah same as for the other, I think this might be a legit fix of a typo; "!!" was removed in the PR
@yannicnoller , same as the other one, It's a valid typeo fix, I meant, that the PR is not fixing any unsound behavior. But, of course, let's accept this change then.
This change should get rid of this confusing error message:
as seen here and here.