Sometimes I don't get to choose the user name assigned to me on servers where I intend to log in frequently. This means that each time I log in to those servers, I have to remember to enter a special user name--until today. Today it occurred to me that I can probably add an entry to $HOME/.ssh/config that sets a different default user name for particular servers. The command man ssh_config explained how. An example config file:

Host buildbox
User shathaway

I can now type ssh buildbox instead of ssh shathaway@buildbox to connect. Since I use ssh very frequently, especially for version control, this is a nice time saver.