clarified comments;
authorwenzelm
Sat, 01 Jun 2024 15:03:13 +0200
changeset 80229 5e32da8238e1
parent 80228 df84e8ff4839
child 80230 cb4b21b7b473
clarified comments;
src/Pure/General/ssh.scala
src/Pure/System/bash.scala
src/Pure/System/isabelle_system.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 =
--- 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) => (),