Move repositories on GitHub without breaking links to PRs
Since it took me way too much time to figure this out, I’ll write it down for future references. I needed to move a git repository from one GitHub repository to another one that already had code, past PRs, etc. It wasn’t a simple rename which would make GitHub redirect everything. It was adding a new history from one repository to another, while not getting rid of the past tags, releases. ...