On 7/9/25 6:17 PM, David Cooper wrote:
I did that.Ray,
I don't think it has (to have) anything to do with any of your existing keys. The gitlab interface gives you a new public key meant specifically for the mirroring instance, and you copy it with the clipboard icon in lower left of the image below ("Copy Public SSH Key").
You then paste that key as a normal SSH key into the Settings -> SSH Keys of the owning github account of the target repository (not deploy key -- i think deploy keys are normally read-only aren't they?)
I did that too. I must have made a mistake last time because github said the key already existed. But I did it just now and there's an extra ssh key that I just added. Wonder what I did wrong?
(I didn't know until now but there's a button that says deploy keys can have write access.)
Anyway, I started the mirroring process again. Let's see how that goes...
Oh, in case any wants to know, the format of the url isn't really clear. What I ended up using was ssh://rtoy@github.com/rtoy/cmucl.git, since rtoy is my github uid. I think; I didn't write it down and gitlab doesn't show it and there doesn't seem to be any way to get it.
Thanks for your help!