On Mon, 26 Nov 2012, Gerwin Klein wrote:
The reasoning (or rather hope) behind the above was that for doing real
non-sense you would have to be on the local network at TUM. So it is
basically a switch back towards the old-fashioned ways of rsh.
I'm fine with that part. I mainly don't want to get the warning emails
for each session. Maybe we should just leave off the line with
/dev/null.
OK, until we get better ideas ~isatest/.ssh/config is like this:
Host *
StrictHostKeyChecking no
So the mails only happen when there is a conflict with earlier implicit
updates of known_hosts, and the situation can be resolved by resetting
that file.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
