# HG changeset patch
# User wenzelm
# Date 1663501184 -7200
# Node ID d9380ef29276ec51248dca9ebe6d61118e402c4f
# Parent  ff0ad0b304ca100cdf33cee47420930e44d8c5f4# Parent  c72c5407a86ff5778f0114166902d028e2702b48
merged

diff -r ff0ad0b304ca -r d9380ef29276 etc/options
--- a/etc/options	Sun Sep 18 13:33:26 2022 +0200
+++ b/etc/options	Sun Sep 18 13:39:44 2022 +0200
@@ -287,21 +287,21 @@
   -- "excluded markup elements for spell-checker (separated by commas)"
 
 
-section "Secure Shell"
+section "Secure Shell (OpenSSH)"
 
-option ssh_batch_mode : bool = true
+public option ssh_batch_mode : bool = true
   -- "enable SSH batch mode (no user interaction)"
 
-option ssh_multiplexing : bool = true
+public option ssh_multiplexing : bool = true
   -- "enable multiplexing of SSH sessions (ignored on Windows)"
 
-option ssh_compression : bool = true
+public option ssh_compression : bool = true
   -- "enable SSH compression"
 
-option ssh_alive_interval : real = 30
+public option ssh_alive_interval : real = 30
   -- "time interval to keep SSH server connection alive (seconds, ignore value < 0)"
 
-option ssh_alive_count_max : int = 3
+public option ssh_alive_count_max : int = 3
   -- "maximum number of messages to keep SSH server connection alive (ignore value < 0)"