bugfix, use database name

diff --git a/helm/matita/dist/fill_db.sh b/helm/matita/dist/fill_db.sh
index e4e98430899f3d78b9d3b247312d86d9ca616965..1ae28d336944f77a77e3b9b7123f264599d9d6ea 100755 (executable)
--- a/helm/matita/dist/fill_db.sh
+++ b/helm/matita/dist/fill_db.sh
@@ -21,31 +21,32 @@ function appendsql()
   echo "$1" >> $SQL
 }
 
-echo "# SQL statements to create Matita DB" > $SQL
+echo "Step 0."
+echo "  Dropping old databases, if any."
+echo "  You can ignore errors output by this step"
+echo "$drop_sql" | $MYSQL -f
+echo "Step 1."
+echo "  Creating database and users."
+echo "# SQL statements to create Matita DB and users" > $SQL
 appendsql "$create_sql;"
 if [ -z "$DBPASS" ]; then
   appendsql "$grant_sql;"
 else
   appendsql "$grant_sql IDENTIFIED BY '$DBPASS';"
 fi
+$MYSQL < $SQL
+echo "Step 2."
+echo "  Creating database structure."
+echo "# SQL statements to create Matita DB structure" > $SQL
 creator_args="table fill index"
 for arg in $creator_args; do
-  for line in `$TABLE_CREATOR $arg all`; do
-    appendsql $line
-  done
+  appendsql "`$TABLE_CREATOR $arg all`"
 done
-
-echo "Step 1."
-echo " Dropping old databases, if any."
-echo " You can ignore errors output by this step"
-echo "$drop_sql" | $MYSQL -f
-echo "Step 2."
-echo "  Creating database structure using SQL statements from $SQL."
-$MYSQL < $SQL
+$MYSQL $DBNAME < $SQL
 echo "Step 3."
 echo "  Filling database with standard library metadata."
 if [ -f "$STDLIB_DATA" ]; then
-  gunzip -c "$STDLIB_DATA" | $MYSQL
+  gunzip -c "$STDLIB_DATA" | $MYSQL $DBNAME
 else
   echo "  Standard library metadata file $STDLIB_DATA not found, skipping this step."
 fi