bug#8886: duplicate names in THANKS?

[Stefano Lattarini]

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                          k...@freefriends.org
  Karl Berry                          k...@gnu.org

Regards,
  Stefano