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