Re: [Savannah-hackers-public] sv host aliases

[Karl Berry]

    you can add something like this to .ssh/config:
    Host dl
      Hostname download.sv.gnu.org

Good thought, that sounds better than /etc/hosts since it's much less
intrusive and doesn't require typing IP address.  Michael, anyone,
objections to me doing that in a day or two?

I'd also like to make the system prompts on the subhosts actually
reflect the hostnames one can type to get to them.  Is that ok?  The
discrepancies are just another source of confusion/error for my poor
beleagured mind ...

Thanks,
k