bash: proper bash_process via SSH;
authorwenzelm
Sat, 01 Jun 2024 15:22:37 +0200
changeset 80232 99ae8c664667
parent 80231 a2cf0318db4a
child 80233 4ac6324a651b
bash: proper bash_process via SSH; getenv: prefer light-weight ssh.execute;
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)