devtools: fix credit script.

Lisa's git name is lower-case, whereas CHANGELOG.md uses upper case, so it doesn't realize she's named a commit already. Signed-off-by: Rusty Russell <[email protected]>
wade1990 · Jul 30, 2019 · 201b531 · 201b531
1 parent b711915
commit 201b531
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/devtools/credit b/devtools/credit
@@ -30,7 +30,7 @@ while read LINE; do
     if [ $(grep -ci -- "$NAME\|$EMAIL" /tmp/prev-authors.$$) = 0 ]; then
 	NOTES="$NOTES""NEW COMMITTER "
     fi
-    if ! grep -q -- "$NAME" /tmp/namers.$$; then
+    if ! grep -qi -- "$NAME" /tmp/namers.$$; then
 	if [ -z "$NAMER" ]; then
 	    NAMER="$NAME"
 	    NOTES="$NOTES""*NEXT NAMER* "