]> matita.cs.unibo.it Git - helm.git/commit
added utility to dump some tables of the db on mowgli
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 16 Jun 2005 09:25:50 +0000 (09:25 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 16 Jun 2005 09:25:50 +0000 (09:25 +0000)
commit5d9c0b5cdda67ac1672b2e0dd83af7fb67a14a34
treeafbdef2b411c701ffc85ff87ac37d7cc10665ef5
parente0694299a43e5df6fcdf6348f48b3a2cda0b30b7
added utility to dump some tables of the db on mowgli
(useful to export metadata to laptops)
helm/ocaml/metadata/dump_db/dump.sh [new file with mode: 0755]