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 <[email protected]>
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                         [email protected]
 Gerald Pfeifer                      [email protected]
 Gerhard Poul                        [email protected]
 Germano Leichsenring                [email protected]
-Gilles Espinasse                    [email protected]
 Glen Lenker                         [email protected]
 Göran Uddeborg                      [email protected]
 Guochun Shi                         [email protected]
--
1.7.4.1.499.g53f9

Reply via email to