src/Pure/General/ssh.scala
changeset 80227 af6b60c75d7d
parent 80226 17a10bea79a1
child 80229 5e32da8238e1
--- a/src/Pure/General/ssh.scala	Sat Jun 01 14:08:04 2024 +0200
+++ b/src/Pure/General/ssh.scala	Sat Jun 01 14:33:38 2024 +0200
@@ -221,9 +221,9 @@
         settings: Boolean = true,  // ignored
         cleanup: () => Unit = () => ()
     ): Bash.Process = {
-      val remote_script1 = Isabelle_System.export_env(user_home = user_home) + remote_script
-      Bash.process(remote_script1, description = description, cwd = cwd, redirect = redirect,
-        cleanup = cleanup, ssh = ssh)
+      Bash.process(
+        Bash.context(remote_script, user_home = user_home),
+        description = description, cwd = cwd, redirect = redirect, cleanup = cleanup, ssh = ssh)
     }
 
     override def execute(remote_script: String,
@@ -233,8 +233,11 @@
       settings: Boolean = true,  // ignored
       strict: Boolean = true
     ): Process_Result = {
-      val remote_script1 = Isabelle_System.export_env(user_home = user_home) + remote_script
-      Isabelle_System.bash(make_command(args_host = true, args = Bash.string(remote_script1)),
+      val script =
+        make_command(
+          args_host = true,
+          args = Bash.string(Bash.context(remote_script, user_home = user_home)))
+      Isabelle_System.bash(script,
         progress_stdout = progress_stdout,
         progress_stderr = progress_stderr,
         redirect = redirect,