Summary
- discontinued unclear timeout (stemming from jEdit JSch setup, see 14782d58a503), to make it work with native Windows ssh.exe;
- proper time values in seconds;
- clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh; discontinued run_scp: use run_sftp instead;
- more robust, notably for macOS (see also ff92d6edff2c);
- back to plain /tmp (despite 1df53737c59b): relevant for ssh on macOS, to avoid error "unix_listener: path too long for Unix domain socket";
- tuned names;
- proper order of platforms, to make it work uniformly on all plaform families;
The file was modified | etc/options (diff) |
The file was modified | src/Pure/General/ssh.scala (diff) |
The file was modified | src/Pure/General/ssh.scala (diff) |
The file was modified | src/Pure/General/ssh.scala (diff) |
The file was modified | src/Pure/General/ssh.scala (diff) |
The file was modified | etc/settings (diff) |
The file was modified | src/Pure/General/ssh.scala (diff) |
The file was modified | src/Pure/Admin/build_release.scala (diff) |