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.

diff --git a/THANKS.in b/THANKS.in
index fbc4153..2e039e3 100644 (file)
--- a/THANKS.in
+++ b/THANKS.in
@@ -207,7 +207,6 @@ Geoff Whale                         geoffw@cse.unsw.EDU.AU
 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