etc/options
changeset 64130 e17c211a0bb6
parent 63986 c7a4b03727ae
child 64308 b00508facb4f
     1.1 --- a/etc/options	Mon Oct 10 11:11:38 2016 +0200
     1.2 +++ b/etc/options	Mon Oct 10 11:48:24 2016 +0200
     1.3 @@ -185,3 +185,21 @@
     1.4  
     1.5  public option completion_limit : int = 40
     1.6    -- "limit for completion within the formal context"
     1.7 +
     1.8 +
     1.9 +section "Secure Shell"
    1.10 +
    1.11 +option ssh_config_dir : string = "~/.ssh"
    1.12 +  -- "SSH configuration directory"
    1.13 +
    1.14 +option ssh_config_file : string = "~/.ssh/config"
    1.15 +  -- "main SSH configuration file"
    1.16 +
    1.17 +option ssh_identity_files : string = "~/.ssh/id_dsa:~/.ssh/id_ecdsa:~/.ssh/id_rsa"
    1.18 +  -- "possible SSH identity files (separated by colons)"
    1.19 +
    1.20 +option ssh_compression : bool = true
    1.21 +  -- "enable SSH compression"
    1.22 +
    1.23 +option ssh_connect_timeout : real = 60
    1.24 +  -- "SSH connection timeout (seconds)"