# HG changeset patch
# User wenzelm
# Date 1663017981 -7200
# Node ID a284c752db3969c501cc2403883d5d59c4096849
# Parent  497e105a4618f42421892eaf0bdc150d2f3d2b48
obsolete;

diff -r 497e105a4618 -r a284c752db39 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"