Add ability to map GitHub IDs to real names

[ChrisTimperley]

Rather than (only) showing the GitHub ID of each contributor to the repo, we can show their real name (and/or Andrew ID).
We can also allow real names to map to more than one GitHub contributor name to tackle cases where someone forgets to update their git config to use their GitHub handle.

To do this, we will need to have some sort of persistence.
A simple database (e.g., SQLite) is probably best for now.
To make this work, we would need to flesh out the admin panel to make it easy for users to add, modify, and remove mappings.