proper treatment of complex multi-line script;
authorwenzelm
Wed, 14 Sep 2022 16:46:00 +0200
changeset 76151 21492610ae5b
parent 76150 5c971c7fc807
child 76152 a95196ef33f0
proper treatment of complex multi-line script;
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)
     }