# 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 \SSH configuration\ text \ - 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