Map github user ids to gitlab user ids

It would be a nice thing to have a custom configured mapping file that gives what would be the Gitlab user id for a Github remote user id. Armed with this, the user references could be prefixed with an @ sign.