tuned output;
authorwenzelm
Fri, 28 Jun 2024 23:53:25 +0200
changeset 80450 4355857e13a6
parent 80449 cba532bf4316
child 80451 e0bd9e4811ad
tuned output;
src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Fri Jun 28 21:01:57 2024 +0200
+++ b/src/Pure/Tools/phabricator.scala	Fri Jun 28 23:53:25 2024 +0200
@@ -498,7 +498,7 @@
         """CREATE USER """ + mysql_user_string +
         """ IDENTIFIED BY """ + SQL.string(mysql_password) + """ PASSWORD EXPIRE NEVER; """ +
         """GRANT ALL ON `""" + (mysql_name + "_%").replace("_", "\\_") +
-        """`.* TO """ + mysql_user_string + ";" +
+        """`.* TO """ + mysql_user_string + "; " +
         """GRANT PROCESS ON *.* TO """ + mysql_user_string + ";")).check
 
     config.execute("config set mysql.user " + Bash.string(mysql_name))