diff -r 17a10bea79a1 -r af6b60c75d7d src/Pure/General/ssh.scala --- 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,