From eb800f1dd90f2b9c8424c71392e225312752f34b Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 13 May 2005 13:00:59 +0000
Subject: [PATCH] sync script among databases

---
 helm/ocaml/metadata/table_creator/sync_db.sh | 28 ++++++++++++++++++++
 1 file changed, 28 insertions(+)
 create mode 100755 helm/ocaml/metadata/table_creator/sync_db.sh

diff --git a/helm/ocaml/metadata/table_creator/sync_db.sh b/helm/ocaml/metadata/table_creator/sync_db.sh
new file mode 100755
index 000000000..7b201382a
--- /dev/null
+++ b/helm/ocaml/metadata/table_creator/sync_db.sh
@@ -0,0 +1,28 @@
+#!/bin/sh
+
+# sync metadata from a source database (usually "mowgli") to a target one
+# (usually "matita")
+# Created:        Fri, 13 May 2005 13:50:16 +0200 zacchiro
+# Last-Modified:  Fri, 13 May 2005 13:50:16 +0200 zacchiro
+
+SOURCE_DB="mowgli"
+TARGET_DB="matita"
+MYSQL_FLAGS="-u helm -h localhost"
+
+MYSQL="mysql $MYSQL_FLAGS -f"
+MYSQLDUMP="mysqldump $MYSQL_FLAGS"
+MYSQLRESTORE="mysqlrestore $MYSQL_FLAGS"
+TABLES=`./table_creator list all`
+DUMP="${SOURCE_DB}_dump.gz"
+
+echo "Dumping source db $SOURCE_DB ..."
+$MYSQLDUMP $SOURCE_DB $TABLES | gzip -c > $DUMP
+echo "Destroying old tables in target db $TARGET_DB ..."
+./table_destructor table all | $MYSQL $TARGET_DB
+echo "Creating table structure in target db $TARGET_DB ..."
+echo "Filling target db $TARGET_DB ..."
+zcat $DUMP | $MYSQL $TARGET_DB
+./table_creator index all | $MYSQL $TARGET_DB
+rm $DUMP
+echo "Done."
+
-- 
2.39.2