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 protected]
Karl Berry [email protected]
Regards,
Stefano
