Credits API: Some repeated names on WordPress credits.php page

[knutsp]

Sergey Biryukov, Mike Schroder and Drew Jaynes are listed under both (group) "Contributing Developers" and (list) "Core Contributors".

They have one thing in common, their nicknames are mixed case (SergeyBiryukov, DH-Shredder, DrewAPicture). All others listed in groups have lowercase nicks.

In core/credits/wp-39.php I see that groups() uses mixed case array keys, but props() uses lowercased keys.

Is there some "no duplicates" or "no repeats" checking in the API that misses those three because of case sensitivity?

[coffee2code]

In 1266:

Credits API: Prevent group members with mixed case names from also being listed as Contributing Developers

Some members via groups() have mixed case names, but names via props() are all lowercase, so the array_diff() didn't filter out some people from getting double props.

Fixes #432