The Names of Github contributors (via pull request) are not displayed on Name List.

[evan0greenup]

The names of github contributors are not displayed on Name List.

[certik]

@evan0greenup can you be specific? That list is automatically generated from git so it should contain everyone. However, I think it only gets updated when we make a release. So if you contributed recently, but we have not make a release, then your name might not be there.

[asmeurer]

The dev docs are updated from master, but the AUTHORS file itself is only updated manually when someone runs ./bin/authors_update.py. We do it before a release, but between releases it is only done when someone thinks about it. It (along with ./bin/mailmap_update.py) requires some manual work to de-duplicate names and emails, which is why it isn't run automatically. If you want to make a PR to sympy running both those scripts and cleaning everything up (it explains what to do), we can merge it.

[asmeurer]

There are some thoughts about doing it automatically sympy/sympy-bot#44. There are some open questions about how to do it.