eliminated pointless option -T: it merely tests ssh config of root, which is not required later;
authorwenzelm
Tue, 17 Dec 2019 13:35:03 +0100
changeset 71295 6aadbd650280
parent 71294 aba1f84a7160
child 71296 71ea54e851ad
eliminated pointless option -T: it merely tests ssh config of root, which is not required later;
src/Doc/System/Phabricator.thy
src/Pure/Tools/phabricator.scala
--- 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>\<open>$HOME/.ssh/config\<close>
   to add a \<^verbatim>\<open>Port\<close> specification for the server machine.
-
-  \<^medskip>
-  Option \<^verbatim>\<open>-T\<close> 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.
 \<close>
 
 end
--- 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)
     })
 }