more rebust setup for Subversion -- assuming that diffusion.ssh-port is only set in phabricator/conf/local/local.json, not in the database;
--- 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(