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