discontinued adhoc change of environment (from c62b99e3ec07), which has been mostly superseded by expand_path / remote_path (from ef6f7e8a018c);
--- a/src/Pure/General/ssh.scala Tue Jan 24 17:25:00 2023 +0100
+++ b/src/Pure/General/ssh.scala Tue Jan 24 17:28:30 2023 +0100
@@ -185,9 +185,11 @@
settings: Boolean = true,
strict: Boolean = true
): Process_Result = {
- val args1 = Bash.string(host) + " " + Bash.string("export USER_HOME=\"$HOME\"\n" + cmd_line)
- run_command("ssh", args = args1, progress_stdout = progress_stdout,
- progress_stderr = progress_stderr, strict = strict)
+ run_command("ssh",
+ args = Bash.string(host) + " " + Bash.string(cmd_line),
+ progress_stdout = progress_stdout,
+ progress_stderr = progress_stderr,
+ strict = strict)
}
override def download_file(