tuned;
authorwenzelm
Fri, 30 Oct 2020 20:45:28 +0100
changeset 72757 f760554a5a29
parent 72754 4be6ae020fc4
child 72758 581d9d74e1e4
tuned;
src/Doc/System/Phabricator.thy
--- a/src/Doc/System/Phabricator.thy	Thu Oct 29 16:07:41 2020 +0100
+++ b/src/Doc/System/Phabricator.thy	Fri Oct 30 20:45:28 2020 +0100
@@ -73,8 +73,8 @@
   (\secref{sec:phabricator-domain}).
 
   Initial experimentation also works on a local host, e.g.\ via
-  VirtualBox\<^footnote>\<open>\<^url>\<open>https://www.virtualbox.org\<close>\<close>. The public domain \<^verbatim>\<open>lvh.me\<close> is
-  used by default: it maps arbitrary subdomains to \<^verbatim>\<open>localhost\<close>.
+  VirtualBox\<^footnote>\<open>\<^url>\<open>https://www.virtualbox.org\<close>\<close>. The Internet domain \<^verbatim>\<open>lvh.me\<close>
+  is used by default: it maps arbitrary subdomains to \<^verbatim>\<open>localhost\<close>.
 
   All administrative commands need to be run as \<^verbatim>\<open>root\<close> user (e.g.\ via
   \<^verbatim>\<open>sudo\<close>). Note that Isabelle refers to user-specific configuration in the
@@ -212,7 +212,7 @@
 \<close>
 
 
-subsection \<open>Public domain name and HTTPS configuration \label{sec:phabricator-domain}\<close>
+subsection \<open>Internet domain name and HTTPS configuration \label{sec:phabricator-domain}\<close>
 
 text \<open>
   So far the Phabricator server has been accessible only on \<^verbatim>\<open>localhost\<close> (via