diff options
| author |  Andres Erbsen <andres@krutt.org> | 2016-06-25 23:10:34 -0400 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2016-06-25 23:10:34 -0400 |
| commit | 794b0fe8f74bb54031ca37ed0f126ecc0b46f2fb (patch) | |
| tree | 8b51df4742b5692e0eab44628ecb9fb8487f3719 /CONTRIBUTORS | |
| parent | 4360c60205d379f349cbfc6e8c0a691a0a4d45fc (diff) | |
Update CONTRIBUTORS
Diffstat (limited to 'CONTRIBUTORS')
| -rw-r--r-- | CONTRIBUTORS | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/CONTRIBUTORS b/CONTRIBUTORS index cf6cd93fa..905edafd1 100644 --- a/CONTRIBUTORS +++ b/CONTRIBUTORS @@ -20,9 +20,6 @@ # Please keep the list sorted. -## This file allows joining different accounts of a single person. -## Cf for instance: git shortlog -nse. More details via: man git shortlog - Adam Chlipala <adamc@csail.mit.edu> <adam@chlipala.net> Andres Erbsen <andreser@mit.edu> Daniel Ziegler <dmz@mit.edu> |