# HG changeset patch
# User wenzelm
# Date 1663453460 -7200
# Node ID c72c5407a86ff5778f0114166902d028e2702b48
# Parent  778152d51e972d21bad5383afb4685efb793f574
show SSH options in PIDE GUI;

diff -r 778152d51e97 -r c72c5407a86f etc/options
--- a/etc/options	Sun Sep 18 00:00:05 2022 +0200
+++ b/etc/options	Sun Sep 18 00:24:20 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)"