]> matita.cs.unibo.it Git - helm.git/commit
now the extractor manager renames the tables (old tables are renamed to _BACKUP)
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 13 May 2005 10:58:40 +0000 (10:58 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 13 May 2005 10:58:40 +0000 (10:58 +0000)
commit8e8dcd3aa99386578b4002a09696884f61941306
tree34cba874f8a5f12df4f7405c353e611364330423
parent0331b47a13331b97e65994c1cdb5298dabc99eb3
now the extractor manager renames the tables (old tables are renamed to _BACKUP)
helm/ocaml/metadata/extractor/extractor.ml
helm/ocaml/metadata/extractor/extractor_manager.ml