obsolete;
authorwenzelm
Mon, 12 Sep 2022 23:26:21 +0200
changeset 76126 a284c752db39
parent 76125 497e105a4618
child 76127 a2b3999c2277
obsolete;
etc/options
--- a/etc/options	Mon Sep 12 23:24:50 2022 +0200
+++ b/etc/options	Mon Sep 12 23:26:21 2022 +0200
@@ -289,15 +289,6 @@
 
 section "Secure Shell"
 
-option ssh_config_dir : string = "$HOME/.ssh"
-  -- "SSH configuration directory"
-
-option ssh_config_file : string = "$HOME/.ssh/config"
-  -- "main SSH configuration file"
-
-option ssh_identity_files : string = "$HOME/.ssh/id_dsa:$HOME/.ssh/id_ecdsa:$HOME/.ssh/id_rsa"
-  -- "possible SSH identity files (separated by colons)"
-
 option ssh_compression : bool = true
   -- "enable SSH compression"