Make it optional to use real names on the server

[johningve]

The automatic registration currently assigns each student a Discord nickname based on the name the student used on Autograder (should be their real name). This behavior should be made optional. However, it should always be possible for the teaching assistants to get the real name of the students.

Proposed solution:

• Add a new config option to enable/disable the use of real names.
• Add a new teaching assistant command to get a student's real name from the database.
• Make existing teaching assistant commands like !next, !list, etc. return real names together with discord usernames.