handle user rename

pietroalbini · pietroalbini · commit 3c711165590e · 2025-04-05T15:18:39.000+02:00
diff --git a/people/PartiallyUntyped.toml b/people/PartiallyUntyped.toml
@@ -1,5 +1,5 @@
 name = "Quinn Sinclair"
-github = "m-rph"
+github = "PartiallyUntyped"
 github-id = 52372765
 zulip-id = 666012
 email = "me@m-rph.dev"
diff --git a/teams/clippy-contributors.toml b/teams/clippy-contributors.toml
@@ -9,7 +9,7 @@ members = [
     "pitaj",
 ]
 alumni = [
-    "m-rph",
+    "PartiallyUntyped",
 ]
 
 [[github]]
