# HG changeset patch
# User wenzelm
# Date 1717246993 -7200
# Node ID 5e32da8238e1af27599200fa54d321d810709d9d
# Parent  df84e8ff48392238100f5d74aaa94d7bea731587
clarified comments;

diff -r df84e8ff4839 -r 5e32da8238e1 src/Pure/General/ssh.scala
--- 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 =
diff -r df84e8ff4839 -r 5e32da8238e1 src/Pure/System/bash.scala
--- 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)
diff -r df84e8ff4839 -r 5e32da8238e1 src/Pure/System/isabelle_system.scala
--- 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) => (),