# HG changeset patch
# User wenzelm
# Date 1573735711 -3600
# Node ID beb781551a6603ce10af3a17c19a0b7fca7ae088
# Parent  7dbadecdc1180cc313fd1053953e3952d35336a4
more sanity checks;

diff -r 7dbadecdc118 -r beb781551a66 src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Thu Nov 14 13:41:50 2019 +0100
+++ b/src/Pure/Tools/phabricator.scala	Thu Nov 14 13:48:31 2019 +0100
@@ -200,8 +200,9 @@
 
     /* users */
 
-    if (name == daemon_user) {
-      error("Clash of installation name with daemon user " + quote(daemon_user))
+    if (name.contains((c: Char) => !(Symbol.is_ascii_letter(c) || Symbol.is_ascii_digit(c))) ||
+        Set("", "ssh", "phd", daemon_user).contains(name)) {
+      error("Bad installation name: " + quote(name))
     }
 
     user_setup(daemon_user, "Phabricator Daemon User", ssh_setup = true)