# HG changeset patch
# User wenzelm
# Date 1663329722 -7200
# Node ID aab9bb081f01a0aac23fdee9bd44624ec740a440
# Parent  e517a38dc0e6f8f2035b8f51ebf6e6b0f94d4972
clarified options;

diff -r e517a38dc0e6 -r aab9bb081f01 etc/options
--- a/etc/options	Fri Sep 16 12:49:04 2022 +0200
+++ b/etc/options	Fri Sep 16 14:02:02 2022 +0200
@@ -289,6 +289,9 @@
 
 section "Secure Shell"
 
+option ssh_batch_mode : bool = true
+  -- "enable SSH batch mode (no user interaction)"
+
 option ssh_multiplexing : bool = true
   -- "enable multiplexing of SSH sessions (ignored on Windows)"
 
diff -r e517a38dc0e6 -r aab9bb081f01 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Fri Sep 16 12:49:04 2022 +0200
+++ b/src/Pure/General/ssh.scala	Fri Sep 16 14:02:02 2022 +0200
@@ -44,11 +44,14 @@
       control_master: Boolean = false,
       control_path: String = ""
     ): List[String] = {
+      val ssh_batch_mode = options.bool("ssh_batch_mode")
       val ssh_compression = options.bool("ssh_compression")
       val ssh_alive_interval = options.real("ssh_alive_interval").round
       val ssh_alive_count_max = options.int("ssh_alive_count_max")
 
-      List("BatchMode=yes", entry("Compression", ssh_compression)) :::
+      List(
+        entry("BatchMode", ssh_batch_mode),
+        entry("Compression", ssh_compression)) :::
       (if (ssh_alive_interval >= 0) List(entry("ServerAliveInterval", ssh_alive_interval)) else Nil) :::
       (if (ssh_alive_count_max >= 0) List(entry("ServerAliveCountMax", ssh_alive_count_max)) else Nil) :::
       (if (port > 0) List(entry("Port", port)) else Nil) :::