maint: remove a name from THANKS.in that is derived from git log
commit8e5292dfb85a4fec2045c00cac5a59bd0c1b8183
authorJim Meyering <meyering@redhat.com>
Sat, 19 Mar 2011 15:55:35 +0000 (19 16:55 +0100)
committerJim Meyering <meyering@redhat.com>
Sun, 20 Mar 2011 15:05:23 +0000 (20 16:05 +0100)
tree6e885f29902f4032de97a076d97b4540857f4d5f
parent7a804b9af4084990a4116964eefb43b2ace4e44a
maint: remove a name from THANKS.in that is derived from git log

The names in THANKS are generated from two sources: the hard-coded
list, THANKS.in, and the names of committers from the git log.
When a contributor on the hard-coded list commits a change,
we remove their now-redundant name from THANKS.in.
* THANKS.in: Remove a now-duplicate name.
THANKS.in