diff options
| -rwxr-xr-x | Tools/scripts/convert-makefile-header.pl | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Tools/scripts/convert-makefile-header.pl b/Tools/scripts/convert-makefile-header.pl index 50aca705f2eb..d23eec1abd83 100755 --- a/Tools/scripts/convert-makefile-header.pl +++ b/Tools/scripts/convert-makefile-header.pl @@ -142,7 +142,7 @@ MAIN: { if(defined($creator)) { my $is_nice=0; for my $c (@$nice_people) { - if($creator=~m"${c}") { + if($creator=~m"${c}"i) { $is_nice=1; last; } |