--- a/src/Pure/General/ssh.scala Sat Jun 01 14:56:24 2024 +0200
+++ b/src/Pure/General/ssh.scala Sat Jun 01 15:03:13 2024 +0200
@@ -218,7 +218,7 @@
description: String = "",
cwd: Path = Path.current,
redirect: Boolean = false,
- settings: Boolean = true, // ignored
+ settings: Boolean = true, // ignored for remote ssh
cleanup: () => Unit = () => ()
): Bash.Process = {
Bash.process(
@@ -230,7 +230,7 @@
progress_stdout: String => Unit = (_: String) => (),
progress_stderr: String => Unit = (_: String) => (),
redirect: Boolean = false,
- settings: Boolean = true, // ignored
+ settings: Boolean = true, // ignored for remote ssh
strict: Boolean = true
): Process_Result = {
val script =
--- a/src/Pure/System/bash.scala Sat Jun 01 14:56:24 2024 +0200
+++ b/src/Pure/System/bash.scala Sat Jun 01 15:03:13 2024 +0200
@@ -80,7 +80,7 @@
description: 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,
cleanup: () => Unit = () => ()): Process =
new Process(script, description, ssh, cwd, env, redirect, cleanup)
--- a/src/Pure/System/isabelle_system.scala Sat Jun 01 14:56:24 2024 +0200
+++ b/src/Pure/System/isabelle_system.scala Sat Jun 01 15:03:13 2024 +0200
@@ -412,7 +412,7 @@
description: String = "",
ssh: SSH.System = SSH.Local,
cwd: Path = Path.current,
- env: JMap[String, String] = settings(),
+ env: JMap[String, String] = settings(), // ignored for remote ssh
redirect: Boolean = false,
input: String = "",
progress_stdout: String => Unit = (_: String) => (),