Use the right username/password

Author: vmcj

.github/jobs/baseinstall.sh

@@ -61,7 +61,7 @@ EOF
 cat ~/.my.cnf
 
 mysql_root "CREATE DATABASE IF NOT EXISTS \`$DATABASE_NAME\` DEFAULT CHARACTER SET utf8mb4 COLLATE utf8mb4_unicode_ci;"
-mysql_root "CREATE USER IF NOT EXISTS \`$DATABASE_NAME\`@'%' IDENTIFIED BY 'domjudge';"
+mysql_root "CREATE USER IF NOT EXISTS 'domjudge'@'%' IDENTIFIED BY 'domjudge';"
 mysql_root "GRANT SELECT, INSERT, UPDATE, DELETE ON \`$DATABASE_NAME\`.* TO 'domjudge'@'%';"
 mysql_root "FLUSH PRIVILEGES;"