Use our standard script to create database

.github/jobs/baseinstall.sh

@@ -54,17 +54,15 @@ password=root
 EOF
 cat ~/.my.cnf
 
-mysql_root "CREATE DATABASE IF NOT EXISTS \`domjudge\` DEFAULT CHARACTER SET utf8mb4 COLLATE utf8mb4_unicode_ci;"
-mysql_root "CREATE USER IF NOT EXISTS \`domjudge\`@'%' IDENTIFIED BY 'domjudge';"
-mysql_root "GRANT SELECT, INSERT, UPDATE, DELETE ON \`domjudge\`.* TO 'domjudge'@'%';"
-mysql_root "FLUSH PRIVILEGES;"
+echo 'unused:sqlserver:domjudge:domjudge:domjudge_db-pw+% #$*)@(!/;,.:3306' > /opt/domjudge/domserver/etc/dbpasswords.secret
+
+/opt/domjudge/domserver/bin/dj_setup_database -uroot -proot create-db-users
 
 # Show some MySQL debugging
 mysql_root "show databases"
 mysql_root "SELECT CURRENT_USER();"
 mysql_root "SELECT USER();"
 mysql_root "SELECT user,host FROM mysql.user"
-echo 'unused:sqlserver:domjudge:domjudge:domjudge_db-pw+% #$*)@(!/;,.:3306' > /opt/domjudge/domserver/etc/dbpasswords.secret
 section_end
 
 if [ "${db}" = "install" ]; then