author | wenzelm |
Fri, 30 Oct 2020 21:10:18 +0100 | |
changeset 72520 | 581d9d74e1e4 |
parent 72519 | f760554a5a29 |
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)) }