Actually, no
need to replace it. $USER is set automatically.
You can run:
$ for SERVER in clematis hawthorn nightshade ortelius willow wolfsbane
yarrow; do ssh $USER(a)$SERVER.toolserver.org test -s /var/mail/$USER &&
echo $SERVER; done
and it will list for you the servers where you
have mail.
Actually, that's only true for those whose username on the
toolserver is the same as on their private box :-). I'd
have to name my username on the toolserver either explicitly
or rely on my ~/.ssh/config:
| Host *.toolserver.org
| User timl
and always escape the second $USER so that it is expanded on
the toolserver.
Tim
I had run the above in the login server. Hadn't noticed you were doing
so from local.