# HG changeset patch
# User wenzelm
# Date 1576525420 -3600
# Node ID 8b745b4d71b55f8d900bede66704493de227928c
# Parent  6a40d06698cb245a381eacc7cd4951b2cf119c44
more rebust setup for Subversion -- assuming that diffusion.ssh-port is only set in phabricator/conf/local/local.json, not in the database;

diff -r 6a40d06698cb -r 8b745b4d71b5 src/Doc/System/Phabricator.thy
--- 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>
diff -r 6a40d06698cb -r 8b745b4d71b5 src/Pure/Tools/phabricator.scala
--- 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(