# HG changeset patch
# User wenzelm
# Date 1576770933 -3600
# Node ID 7c27a379190f843ed799706b1cc95a1cde3f7256
# Parent  0256ce61f4053f98b635c3e249a6318bba009d81
tuned documentation;

diff -r 0256ce61f405 -r 7c27a379190f src/Doc/System/Phabricator.thy
--- a/src/Doc/System/Phabricator.thy	Thu Dec 19 16:49:29 2019 +0100
+++ b/src/Doc/System/Phabricator.thy	Thu Dec 19 16:55:33 2019 +0100
@@ -183,8 +183,9 @@
 subsection \<open>SSH configuration\<close>
 
 text \<open>
-  SSH configuration is optional, but important to access hosted repositories
-  with public-key authentication.
+  SSH configuration is important to access hosted repositories with public-key
+  authentication. It is done by a separate tool, because it affects the
+  operating-system and all installations of Phabricator simultaneously.
 
   The subsequent configuration is convenient (and ambitious): it takes away
   the standard port 22 from the operating system and assigns it to