diff --git a/.github/jobs/baseinstall.sh b/.github/jobs/baseinstall.sh
index f1997f58b2..9adf0a6628 100755
--- a/.github/jobs/baseinstall.sh
+++ b/.github/jobs/baseinstall.sh
@@ -68,7 +68,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 'domjudge'@'%' 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;"