diff options
Diffstat (limited to 'etc/author-blacklist')
| -rw-r--r-- | etc/author-blacklist | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/etc/author-blacklist b/etc/author-blacklist index a878ed429..a2df8569f 100644 --- a/etc/author-blacklist +++ b/etc/author-blacklist @@ -15,7 +15,8 @@ Jade Philipoom Andres Erbsen -Adam +adam.chlipala +Adam Chlipala Chlipala csail mit-plv |