diff options
| -rwxr-xr-x | devtools/credits.pl | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/devtools/credits.pl b/devtools/credits.pl index 1fd40dbab2..e8cb1154e7 100755 --- a/devtools/credits.pl +++ b/devtools/credits.pl @@ -359,6 +359,9 @@ sub add_person { my $min_name_width = length $desc > 0 ? $max_name_width : 0; $name = $nick if $name eq ""; $name = html_entities_to_ascii($name); + if (length $name > $max_name_width) { + print STDERR "Warning: max_name_width is too small (" . $max_name_width . " < " . (length $name) . " for \"" . $name. "\")\n"; + } $desc = html_entities_to_ascii($desc); $tab = " " x ($section_level * 2 + 1); |