# HG changeset patch
# User wenzelm
# Date 1576098574 -3600
# Node ID 5212ca49598a4f0d83fbfe87a95391c114465a1a
# Parent  6b8cbdc9713b1406278b9cea7f59449d2cfa1423
more robust;

diff -r 6b8cbdc9713b -r 5212ca49598a src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Wed Dec 11 21:49:24 2019 +0100
+++ b/src/Pure/Tools/phabricator.scala	Wed Dec 11 22:09:34 2019 +0100
@@ -311,7 +311,8 @@
     Isabelle_System.bash("mysql --user=" + Bash.string(mysql_root_user) +
       " --password=" + Bash.string(mysql_root_password) + " --execute=" +
       Bash.string(
-        """CREATE USER IF NOT EXISTS """ + mysql_user_string +
+        """DROP USER IF EXISTS """ + mysql_user_string + "; " +
+        """CREATE USER """ + mysql_user_string +
         """ IDENTIFIED BY """ + SQL.string(mysql_password) + """ PASSWORD EXPIRE NEVER; """ +
         """GRANT ALL ON `""" + (mysql_name + "_%").replace("_", "\\_") +
         """`.* TO """ + mysql_user_string + ";")).check