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)"