# HG changeset patch
# User wenzelm
# Date 1705179016 -3600
# Node ID a49db426ffd4c44844ce26b52ce69e10cf96e7dd
# Parent  590a01e3efb49a259520224c11b03a603f2eaecf
refer to "localhost" as pro-forma domain;

diff -r 590a01e3efb4 -r a49db426ffd4 src/Doc/System/Phabricator.thy
--- a/src/Doc/System/Phabricator.thy	Fri Jan 12 17:00:35 2024 +0100
+++ b/src/Doc/System/Phabricator.thy	Sat Jan 13 21:50:16 2024 +0100
@@ -74,8 +74,10 @@
   (\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 Internet 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 proforma domain
+  \<^verbatim>\<open>localhost\<close> is used by default: it maps arbitrary subdomains to the usual
+  \<^verbatim>\<open>localhost\<close> address. This allows to use e.g.
+  \<^verbatim>\<open>http://phabricator-vcs.localhost\<close> for initial setup as described below.
 
   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
@@ -216,9 +218,9 @@
 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
-  the alias \<^verbatim>\<open>lvh.me\<close>). Proper configuration of a public Internet domain name
-  (with HTTPS certificate from \<^emph>\<open>Let's Encrypt\<close>) works as follows.
+  So far the Phabricator server has been accessible only on \<^verbatim>\<open>localhost\<close>.
+  Proper configuration of a public Internet domain name (with HTTPS
+  certificate from \<^emph>\<open>Let's Encrypt\<close>) works as follows.
 
     \<^item> Register a subdomain (e.g.\ \<^verbatim>\<open>vcs.example.org\<close>) as an alias for the IP
     address of the underlying Linux host. This usually works by some web
diff -r 590a01e3efb4 -r a49db426ffd4 src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Fri Jan 12 17:00:35 2024 +0100
+++ b/src/Pure/Tools/phabricator.scala	Sat Jan 13 21:50:16 2024 +0100
@@ -439,7 +439,7 @@
 
     if (!apache_sites.is_dir) error("Bad Apache sites directory " + apache_sites)
 
-    val server_name = phabricator_name(name = name, ext = "lvh.me")  // alias for "localhost" for testing
+    val server_name = phabricator_name(name = name, ext = "localhost")  // alias for "localhost" for testing
     val server_url = "http://" + server_name
 
     File.write(apache_sites + Path.basic(isabelle_phabricator_name(name = name, ext = "conf")),