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.
Gerald Pfeifer gerald@pfeifer.com
Gerhard Poul gpoul@gnu.org
Germano Leichsenring germano@jedi.cs.kobe-u.ac.jp
-Gilles Espinasse g.esp@free.fr
Glen Lenker glen.lenker@gmail.com
Göran Uddeborg goeran@uddeborg.se
Guochun Shi gshi@ncsa.uiuc.edu