# HG changeset patch # User wenzelm # Date 1576586103 -3600 # Node ID 6aadbd6502801dfd33c7fff3df61561360402676 # Parent aba1f84a71607a62553af54e7aea9d6b812b996e eliminated pointless option -T: it merely tests ssh config of root, which is not required later; diff -r aba1f84a7160 -r 6aadbd650280 src/Doc/System/Phabricator.thy --- a/src/Doc/System/Phabricator.thy Tue Dec 17 08:05:59 2019 +0100 +++ b/src/Doc/System/Phabricator.thy Tue Dec 17 13:35:03 2019 +0100 @@ -480,7 +480,6 @@ Options are: -p PORT sshd port for Phabricator servers (default: 2222) -q PORT sshd port for the operating system (default: 22) - -T test the ssh service for each Phabricator installation Configure ssh service for all Phabricator installations: a separate sshd is run in addition to the one of the operating system, and ports need to @@ -514,11 +513,6 @@ Redirecting the operating system sshd to port 222 requires some care: it requires to adjust the remote login procedure, e.g.\ in \<^verbatim>\$HOME/.ssh/config\ to add a \<^verbatim>\Port\ specification for the server machine. - - \<^medskip> - Option \<^verbatim>\-T\ tests the SSH connection by communicating via Conduit. This - requires to install the public key of the Linux root in some Phabricator - user profile, e.g.\ for the administrator. \ end diff -r aba1f84a7160 -r 6aadbd650280 src/Pure/Tools/phabricator.scala --- a/src/Pure/Tools/phabricator.scala Tue Dec 17 08:05:59 2019 +0100 +++ b/src/Pure/Tools/phabricator.scala Tue Dec 17 13:35:03 2019 +0100 @@ -706,7 +706,6 @@ def phabricator_setup_ssh( server_port: Int = default_server_port, system_port: Int = default_system_port, - test_server: Boolean = false, progress: Progress = No_Progress) { Linux.check_system_root() @@ -785,14 +784,6 @@ progress.echo("phabricator " + quote(config.name) + " port " + server_port) config.execute("config set diffusion.ssh-port " + Bash.string(server_port.toString)) if (server_port == 22) config.execute("config delete diffusion.ssh-port") - - if (test_server) { - progress.bash( - """unset DISPLAY - echo "{}" | ssh -p """ + Bash.string(server_port.toString) + - " -o StrictHostKeyChecking=false " + - Bash.string(config.name) + """@localhost conduit conduit.ping""").print - } } } @@ -805,7 +796,6 @@ { var server_port = default_server_port var system_port = default_system_port - var test_server = false val getopts = Getopts(""" @@ -814,7 +804,6 @@ Options are: -p PORT sshd port for Phabricator servers (default: """ + default_server_port + """) -q PORT sshd port for the operating system (default: """ + default_system_port + """) - -T test the ssh service for each Phabricator installation Configure ssh service for all Phabricator installations: a separate sshd is run in addition to the one of the operating system, and ports need to @@ -825,8 +814,7 @@ stored ssh keys. """, "p:" -> (arg => server_port = Value.Int.parse(arg)), - "q:" -> (arg => system_port = Value.Int.parse(arg)), - "T" -> (_ => test_server = true)) + "q:" -> (arg => system_port = Value.Int.parse(arg))) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() @@ -834,7 +822,6 @@ val progress = new Console_Progress phabricator_setup_ssh( - server_port = server_port, system_port = system_port, test_server = test_server, - progress = progress) + server_port = server_port, system_port = system_port, progress = progress) }) }