# HG changeset patch
# User wenzelm
# Date 1663101401 -7200
# Node ID e8d4013c49d1b9f924de52aab4f4887db3cb3e8f
# Parent  e7497a1de8b97eb9ac888a5120fa9915d01cb68f
more robust adhoc shell script: work with Isabelle_System.export_isabelle_identifier;

diff -r e7497a1de8b9 -r e8d4013c49d1 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Tue Sep 13 12:30:37 2022 +0000
+++ b/src/Pure/General/ssh.scala	Tue Sep 13 22:36:41 2022 +0200
@@ -170,7 +170,8 @@
       settings: Boolean = true,
       strict: Boolean = true
     ): Process_Result = {
-      val args1 = Bash.string(host) + " env " + Bash.string("USER_HOME=\"$HOME\"") + " " + cmd_line
+      val args1 =
+        Bash.string(host) + " export " + Bash.string("USER_HOME=\"$HOME\"") + "\n" + cmd_line
       run_command("ssh", args = args1, progress_stdout = progress_stdout,
         progress_stderr = progress_stderr, strict = strict)
     }