# HG changeset patch # User wenzelm # Date 1716990675 -7200 # Node ID f2fa6753c3e2e6be9bbd2c355f85880cfd7b1489 # Parent 5f053991315c4cd8c712743663d699d0b320c0bb tuned comments; diff -r 5f053991315c -r f2fa6753c3e2 src/Pure/General/ssh.scala --- a/src/Pure/General/ssh.scala Sat May 25 20:26:06 2024 +0200 +++ b/src/Pure/General/ssh.scala Wed May 29 15:51:15 2024 +0200 @@ -1,7 +1,7 @@ /* Title: Pure/General/ssh.scala Author: Makarius -SSH client on OpenSSH command-line tools, preferably with connection +SSH client on top of OpenSSH command-line tools, preferably with connection multiplexing, but this does not work on Windows. */