more rebust setup for Subversion -- assuming that diffusion.ssh-port is only set in phabricator/conf/local/local.json, not in the database;
authorwenzelm
Mon, 16 Dec 2019 20:43:40 +0100
changeset 71501 8b745b4d71b5
parent 71500 6a40d06698cb
child 71502 8f3940150493
more rebust setup for Subversion -- assuming that diffusion.ssh-port is only set in phabricator/conf/local/local.json, not in the database;
src/Doc/System/Phabricator.thy
src/Pure/Tools/phabricator.scala
--- a/src/Doc/System/Phabricator.thy	Mon Dec 16 19:58:11 2019 +0100
+++ b/src/Doc/System/Phabricator.thy	Mon Dec 16 20:43:40 2019 +0100
@@ -504,10 +504,12 @@
   remains important for remote administration of the machine.
 
   \<^medskip>
-  Options \<^verbatim>\<open>-p\<close> and \<^verbatim>\<open>-q\<close> allow to change the port assignment for both servers.
-  A common scheme is \<^verbatim>\<open>-p 22 -q 222\<close> to leave the standard port to
+  Options \<^verbatim>\<open>-p\<close> and \<^verbatim>\<open>-q\<close> allow to change the port assignment for both
+  servers. A common scheme is \<^verbatim>\<open>-p 22 -q 222\<close> to leave the standard port to
   Phabricator, to simplify the ssh URL that users will see for remote
-  repository clones.
+  repository clones.\<^footnote>\<open>For the rare case of hosting Subversion repositories,
+  port 22 is de-facto required. Otherwise Phabricator presents malformed
+  \<^verbatim>\<open>svn+ssh\<close> URLs with port specification.\<close>
 
   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>
--- a/src/Pure/Tools/phabricator.scala	Mon Dec 16 19:58:11 2019 +0100
+++ b/src/Pure/Tools/phabricator.scala	Mon Dec 16 20:43:40 2019 +0100
@@ -784,6 +784,7 @@
     for (config <- configs) {
       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(