Subject: duplicate names in THANKS?

From: Stefano Lattarini <[email-masked]>
Date: Fri, 17 Jun 2011 22:10:09 +0200

OK, this is just a silly cosmetic issue, but maybe you'd like to know
about it anyway:

  $ make THANKS
    GEN    THANKS
  ./thanks-gen: THANKS.in: duplicate name: Karl Berry
  ./thanks-gen: THANKS.in: duplicate name: Karl Heuer
  ./thanks-gen: THANKS.in: duplicate name: Stéphane Raimbault

  $ grep 'Karl Berry' THANKS
  Karl Berry                          [email-masked]
  Karl Berry                          [email-masked]

Regards,
  Stefano