src/Pure/Tools/phabricator.scala
changeset 72520 581d9d74e1e4
parent 72494 ef2082c41cd0
child 72521 354bfab78cbf
--- a/src/Pure/Tools/phabricator.scala	Fri Oct 30 20:45:28 2020 +0100
+++ b/src/Pure/Tools/phabricator.scala	Fri Oct 30 21:10:18 2020 +0100
@@ -248,7 +248,7 @@
 
     /* users */
 
-    if (name.contains((c: Char) => !(Symbol.is_ascii_letter(c) || Symbol.is_ascii_digit(c))) ||
+    if (name.exists((c: Char) => !(Symbol.is_ascii_letter(c) || Symbol.is_ascii_digit(c))) ||
         Set("", "ssh", "phd", "dump", daemon_user).contains(name)) {
       error("Bad installation name: " + quote(name))
     }