FR: better error for ssh hostname changes #1507
Description
I recently tried to use jj to push to github. The error I got was very perplexing to me. In particular I saw this.
[sonmi]~/dev/protobuf$ jj git push
Branch changes to push to origin:
Add branch test_jj to 5a9dbd9a4edc
Error: invalid or unknown remote ssh hostkey; class=Ssh (23); code=Certificate (-17)
Hint: Jujutsu uses libssh2, which doesn't respect ~/.ssh/config. Does `ssh -F /dev/null` to the host work?
I eventually traced this down to the recent github host changing
[sonmi]~/dev$ git clone git@github.com:fowles/abseil-hello.git
Cloning into 'abseil-hello'...
The authenticity of host 'github.com (140.82.114.3)' can't be established.
ED25519 key fingerprint is XXXXXXXXXXXXX
This key is not known by any other names.
Are you sure you want to continue connecting (yes/no/[fingerprint])? yes
Warning: Permanently added 'github.com' (ED25519) to the list of known hosts.
Warning: the ED25519 host key for 'github.com' differs from the key for the IP address '140.82.114.3'
Offending key for IP in /usr/local/google/home/kfm/.ssh/known_hosts:6
Are you sure you want to continue connecting (yes/no)? yes
so this fixed it, but an error message that told me something more (or better yet gave me the prompt that git does) would be awesome.