src/Doc/System/Phabricator.thy
changeset 71538 2217c731d228
parent 71532 7c27a379190f
child 71556 3c4c171344f4
--- a/src/Doc/System/Phabricator.thy	Fri Dec 20 15:21:25 2019 +0100
+++ b/src/Doc/System/Phabricator.thy	Fri Dec 20 15:24:34 2019 +0100
@@ -267,11 +267,13 @@
     \<^enum> Multiple \<^emph>\<open>MySQL databases\<close> with a common prefix derived from the
     installation name --- the same name is used as database user name.
 
-  The root user may invoke \<^verbatim>\<open>/usr/local/bin/isabelle-phabricator-dump\<close>
-  to create a complete database dump within the root directory. Afterwards it
-  is sufficient to make a conventional \<^bold>\<open>file-system backup\<close> of everything. To
+  The root user may invoke \<^verbatim>\<open>/usr/local/bin/isabelle-phabricator-dump\<close> to
+  create a complete database dump within the root directory. Afterwards it is
+  sufficient to make a conventional \<^bold>\<open>file-system backup\<close> of everything. To
   restore the database state, see the explanations on \<^verbatim>\<open>mysqldump\<close> in
-  \<^url>\<open>https://secure.phabricator.com/book/phabricator/article/configuring_backups\<close>.
+  \<^url>\<open>https://secure.phabricator.com/book/phabricator/article/configuring_backups\<close>;
+  some background information is in
+  \<^url>\<open>https://secure.phabricator.com/book/phabflavor/article/so_many_databases\<close>.
 
   \<^medskip> The following command-line tools are particularly interesting for advanced
   database maintenance (within the Phabricator root directory):