diff options
author | Martin Weinelt <mweinelt@users.noreply.github.com> | 2022-08-11 11:30:13 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2022-08-11 11:30:13 +0200 |
commit | 1805216b8ebab0c266e769df31b7ed4f35aa2452 (patch) | |
tree | 2f14dc953fdb7ae5761d6b640177c3e80d6ec50d /maintainers | |
parent | 439f25de4d6b919d4a05fd552359736b7a2a283d (diff) | |
parent | 70749cfe656857fa2476b0fe24aea3cf48885a76 (diff) |
Merge pull request #185879 from ChrisPattison/galois
Diffstat (limited to 'maintainers')
-rw-r--r-- | maintainers/maintainer-list.nix | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/maintainers/maintainer-list.nix b/maintainers/maintainer-list.nix index 87639fc55d48..d51c11e14914 100644 --- a/maintainers/maintainer-list.nix +++ b/maintainers/maintainer-list.nix @@ -2314,6 +2314,12 @@ githubId = 811527; name = "Christopher Jefferson"; }; + chrispattison = { + email = "chpattison@gmail.com"; + github = "ChrisPattison"; + githubId = 641627; + name = "Chris Pattison"; + }; chrispickard = { email = "chrispickard9@gmail.com"; github = "chrispickard"; |