Re: update user brobecke's public SSH key

[Joel Brobecker <brobecker@adacore.com>]

> > Thanks Mark. Unfortunately, these don't work:
> > 
> >     $ ssh sourceware.org replacekey < .ssh/id_rsa.pub
> >     bash: replacekey: command not found
> >     $ ssh sourceware.org appendkey < .ssh/id_rsa.pub
> >     bash: appendkey: command not found
> 
> That is odd. The user brobecke shouldn't have a bash shell.  Could it
> be that ssh is using another account for which you have a real shell?
> Could you try the above with an explicit brobecke@sourceware.org ?

Headslap. I'm an idiot...

Thanks a lot for pointing me in the right direction, Mark. For
sourceware.org, because I have access to two accounts ("brobecke"
is my restricted user account for pushing commits, while "gdbadmin"
is a shared account for GDB admin stuff, and in particular for
releases). Because I was doing "ssh gdbadmin@sourceware" a lot,
I thought it would be more efficient to configure my SSH to
use gdbadmin by default when ssh-ing to sourceware, and then
force "brobecke" back in my git repositories. That works very
well until the day you miss the implication on the instructions
above.

I'm happy to confirm that...

    $ ssh brobecke@sourceware.org replacekey < .ssh/id_rsa.pub

... worked like a charm. From there, I removed the old key from
my agent, and was able to fetch from GDB, so I think it's all set.

Thanks again!

-- 
Joel