src/Pure/General/ssh.scala
Sat, 14 Jun 2025 14:31:54 +0200 wenzelm clarified signature;
Tue, 06 May 2025 16:52:39 +0200 wenzelm clarified signature;
Tue, 18 Mar 2025 19:07:26 +0100 wenzelm SSH connections allow zsh as well: this happens to work with the existing Bash.char / Bach.string operations;
Wed, 12 Feb 2025 00:40:57 +0100 wenzelm removed unused imports;
Fri, 28 Jun 2024 11:37:13 +0200 wenzelm tuned;
Sat, 01 Jun 2024 21:49:50 +0200 wenzelm clarified signature: more explicit types;
less more (0) -100 -30 -10 -6 tip