src/Pure/Tools/phabricator.scala
changeset 80450 4355857e13a6
parent 80224 db92e0b6a11a
child 81717 114449035ec6
equal deleted inserted replaced
80449:cba532bf4316 80450:4355857e13a6
   496       Bash.string(
   496       Bash.string(
   497         """DROP USER IF EXISTS """ + mysql_user_string + "; " +
   497         """DROP USER IF EXISTS """ + mysql_user_string + "; " +
   498         """CREATE USER """ + mysql_user_string +
   498         """CREATE USER """ + mysql_user_string +
   499         """ IDENTIFIED BY """ + SQL.string(mysql_password) + """ PASSWORD EXPIRE NEVER; """ +
   499         """ IDENTIFIED BY """ + SQL.string(mysql_password) + """ PASSWORD EXPIRE NEVER; """ +
   500         """GRANT ALL ON `""" + (mysql_name + "_%").replace("_", "\\_") +
   500         """GRANT ALL ON `""" + (mysql_name + "_%").replace("_", "\\_") +
   501         """`.* TO """ + mysql_user_string + ";" +
   501         """`.* TO """ + mysql_user_string + "; " +
   502         """GRANT PROCESS ON *.* TO """ + mysql_user_string + ";")).check
   502         """GRANT PROCESS ON *.* TO """ + mysql_user_string + ";")).check
   503 
   503 
   504     config.execute("config set mysql.user " + Bash.string(mysql_name))
   504     config.execute("config set mysql.user " + Bash.string(mysql_name))
   505     config.execute("config set mysql.pass " + Bash.string(mysql_password))
   505     config.execute("config set mysql.pass " + Bash.string(mysql_password))
   506 
   506