# HG changeset patch
# User wenzelm
# Date 1717247506 -7200
# Node ID cb4b21b7b473d7784b51e4fe9fc11adba1c9beeb
# Parent  5e32da8238e1af27599200fa54d321d810709d9d
support bash via SSH;

diff -r 5e32da8238e1 -r cb4b21b7b473 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Sat Jun 01 15:03:13 2024 +0200
+++ b/src/Pure/System/progress.scala	Sat Jun 01 15:11:46 2024 +0200
@@ -93,15 +93,16 @@
   override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
 
   final def bash(script: String,
+    ssh: SSH.System = SSH.Local,
     cwd: Path = Path.current,
-    env: JMap[String, String] = Isabelle_System.settings(),
+    env: JMap[String, String] = Isabelle_System.settings(),  // ignored for remote ssh
     redirect: Boolean = false,
     echo: Boolean = false,
     watchdog: Time = Time.zero,
     strict: Boolean = true
   ): Process_Result = {
     val result =
-      Isabelle_System.bash(script, cwd = cwd, env = env, redirect = redirect,
+      Isabelle_System.bash(script, ssh = ssh, cwd = cwd, env = env, redirect = redirect,
         progress_stdout = echo_if(echo, _),
         progress_stderr = echo_if(echo, _),
         watchdog = if (watchdog.is_zero) None else Some((watchdog, _ => stopped)),