[PATCH] maint: remove a name from THANKS.in that is derived from git log

[Jim Meyering]

I noticed this warning go by:

  $ rm THANKS; make THANKS
    GEN      THANKS
  ./thanks-gen: THANKS.in: duplicate name: Gilles Espinasse

Here's the fix:

>From edd8d8ec6d244307655e6086d4e30f6d524ddf23 Mon Sep 17 00:00:00 2001
From: Jim Meyering <address@hidden>
Date: Sat, 19 Mar 2011 16:55:35 +0100
Subject: [PATCH] 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 |    1 -
 1 files changed, 0 insertions(+), 1 deletions(-)

diff --git a/THANKS.in b/THANKS.in
index fbc4153..2e039e3 100644
--- a/THANKS.in
+++ b/THANKS.in
@@ -207,7 +207,6 @@ Geoff Whale                         address@hidden
 Gerald Pfeifer                      address@hidden
 Gerhard Poul                        address@hidden
 Germano Leichsenring                address@hidden
-Gilles Espinasse                    address@hidden
 Glen Lenker                         address@hidden
 Göran Uddeborg                      address@hidden
 Guochun Shi                         address@hidden
--
1.7.4.1.499.g53f9