diff options
| -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> |