# HG changeset patch
# User wenzelm
# Date 1663166760 -7200
# Node ID 21492610ae5b8e812483f8a708c2a33b8f9f785a
# Parent  5c971c7fc807f2d2de85f59c38ea3ef928bac4df
proper treatment of complex multi-line script;

diff -r 5c971c7fc807 -r 21492610ae5b src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Wed Sep 14 15:57:47 2022 +0200
+++ b/src/Pure/General/ssh.scala	Wed Sep 14 16:46:00 2022 +0200
@@ -154,9 +154,9 @@
 
     /* init and exit */
 
-    val user_home: String =
-      run_ssh(master = control_master, args = "printenv HOME \";\" printenv SHELL").check.out_lines
-      match {
+    val user_home: String = {
+      val args = Bash.string("printenv HOME\nprintenv SHELL")
+      run_ssh(master = control_master, args = args).check.out_lines match {
         case List(user_home, shell) =>
           if (shell.endsWith("/bash")) user_home
           else {
@@ -164,6 +164,7 @@
           }
         case _ => error("Malformed remote environment for " + quote(toString))
       }
+    }
 
     val settings: JMap[String, String] = JMap.of("HOME", user_home, "USER_HOME", user_home)
 
@@ -180,8 +181,7 @@
       settings: Boolean = true,
       strict: Boolean = true
     ): Process_Result = {
-      val args1 =
-        Bash.string(host) + " export " + Bash.string("USER_HOME=\"$HOME\"") + "\n" + cmd_line
+      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)
     }