# HG changeset patch
# User wenzelm
# Date 1604088618 -3600
# Node ID 581d9d74e1e4623798a849733ac3b2e0d66d5bbe
# Parent  f760554a5a295ef3847de38be64a03d2c6e3abf4
tuned --- make IntelliJ IDEA happy;

diff -r f760554a5a29 -r 581d9d74e1e4 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))
     }