sharing ssh agency

For whatever reason, lots of default shell setups make it hard to share SSH agents and their list of authenticated keys. Here's my fix:

In .bashrc:

################
## Check for ssh-agent, and start one if necessary
## rsm 2020-09-12 (but from 2016 or earlier)
if [ -e ${HOME}/.ssh/agent.conf ] ; then
    source ${HOME}/.ssh/agent.conf > /dev/null
fi
if [ "${SSH_AGENT_PID}" ] && ps -p ${SSH_AGENT_PID} > /dev/null &&
       [ ${SSH_AUTH_SOCK} ] && [ -e ${SSH_AUTH_SOCK} ] ; then
    true
else
    mask=$(umask)
    umask 0077
    ssh-agent -t 8d | sed s/^echo/#echo/ >| ${HOME}/.ssh/agent.conf
    umask ${mask}
    source ${HOME}/.ssh/agent.conf
fi

The fancy redirect operator >| overrides the noclobber shell option, which I must have needed at some point.