Migrate this repository to the UIS GitLab service?

[mgkuhn]

@barneybrown suggested in #91 that we should move this entire repository over to the UIS GitLab service “and pick up from there”.

So out of curiosity, I have just tried a test import of this repo to my space on UIS GitLab, to get an idea of what is involved and how this works.

The import process does indeed appear to migrate not just the repo but also all the issues, pull requests and comments. However they now all say “created ... years ago by Markus Kuhn” (i.e., the person doing the import) and the actual creator of the issue/PR/comment is then only mentioned in the first line of the migrated text, as in “Created by: rjw57” in e.g. this comment by @rjw57.

I had hoped that at least some users here would already have gone to https://gitlab.developers.cam.ac.uk/-/profile/account and there under “Social sign-in” have connected their GitHub account with their UIS GitLab account. Has anyone here (other than me) who has opened a ticket here done that already? Or does such linking not actually cause comments to be migrated under the respective user’s name? Because even my own migrated issue is prefixed with “Created by: mgkuhn”.

@rjw57 Is the full migration of user identities during a GitHub-to-USI-GitLab import actually possible, and do I simply not have the right permissions to do so?