tuned --- make IntelliJ IDEA happy;
authorwenzelm
Fri, 30 Oct 2020 21:10:18 +0100
changeset 72758 581d9d74e1e4
parent 72757 f760554a5a29
child 72759 354bfab78cbf
tuned --- make IntelliJ IDEA happy;
src/Pure/Tools/phabricator.scala
--- 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))
     }