diff options
Diffstat (limited to 'tools')
-rwxr-xr-x | tools/update-thanks | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/update-thanks b/tools/update-thanks index 27932f94..b0321e32 100755 --- a/tools/update-thanks +++ b/tools/update-thanks | |||
@@ -34,7 +34,7 @@ git log --pretty='%an' "$since.." | sort -u | while read first last rest | |||
34 | do | 34 | do |
35 | if [ -n "$first" -a -n "$last" -a -z "$rest" ] | 35 | if [ -n "$first" -a -n "$last" -a -z "$rest" ] |
36 | then | 36 | then |
37 | if ! grep -q "^$first $last$" AUTHORS THANKS.in | 37 | if ! grep -q -i "^$first $last$" AUTHORS THANKS.in |
38 | then | 38 | then |
39 | echo "$first $last" >> THANKS.in | 39 | echo "$first $last" >> THANKS.in |
40 | fi | 40 | fi |