fix: remove user PartiallyUntyped#2184
Conversation
Dry-run check results |
AFAICT it's not a rename, the contributor's account got deleted or something based on the log:
|
jieyouxu
left a comment
There was a problem hiding this comment.
Looking at https://lib.rs/~PartiallyUntyped and https://github.com/PartiallyUntyped, their account does not seem to exist anymore. Waiting for confirmation from clippy team.
Co-authored-by: Marco Ieni <11428655+marcoieni@users.noreply.github.com>
|
I also think the user was removed. If it was renamed, github should redirect afaik. |
|
Sure, let's merge to unblock CI. |
|
Yeah, seems reasonable. |
Asking clippy team in #clippy > Removing `PartiallyUntyped` from clippy-contributors alumni |
|
I think that she left Github (although not sure why), I'll try to email her asking if this is correct. |
summary
User PartiallyUntyped doesn't exist, as we're getting a failure in CI for one of the PRs #2149