# HG changeset patch
# User wenzelm
# Date 1717248157 -7200
# Node ID 99ae8c66466704cf0e2360fe38657f6a4287cffb
# Parent  a2cf0318db4a56d82eff54582e3e753c899ccaf6
bash: proper bash_process via SSH;
getenv: prefer light-weight ssh.execute;

diff -r a2cf0318db4a -r 99ae8c664667 src/Pure/System/other_isabelle.scala
--- a/src/Pure/System/other_isabelle.scala	Sat Jun 01 15:13:03 2024 +0200
+++ b/src/Pure/System/other_isabelle.scala	Sat Jun 01 15:22:37 2024 +0200
@@ -56,7 +56,7 @@
     echo: Boolean = false,
     strict: Boolean = true
   ): Process_Result = {
-    ssh.execute(bash_context(script, cwd = cwd),
+    ssh.bash(bash_context(script, cwd = cwd),
       progress_stdout = progress.echo_if(echo, _),
       progress_stderr = progress.echo_if(echo, _),
       redirect = redirect,
@@ -65,7 +65,8 @@
   }
 
   def getenv(name: String): String =
-    bash("bin/isabelle getenv -b " + Bash.string(name)).check.out
+    ssh.execute(bash_context("bin/isabelle getenv -b " + Bash.string(name)),
+      settings = false).check.out
 
   val settings: Isabelle_System.Settings = (name: String) => getenv(name)