# HG changeset patch
# User wenzelm
# Date 1576851874 -3600
# Node ID 2217c731d228f93d3dc69c344147c8e355608c59
# Parent  4642a81f59139bdab9e1c3b64d8ff6c5c8b3c42e
tuned documentation;

diff -r 4642a81f5913 -r 2217c731d228 src/Doc/System/Phabricator.thy
--- 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):