]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 11d8128) | patch
added new extractor based on MetadataDb.index_obj
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 3 May 2005 17:12:49 +0000 (17:12 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 3 May 2005 17:12:49 +0000 (17:12 +0000)
commit53a481cfc7546504db6005b6f29fe30c3d9eabc7
treeca1be20c1289e744378b485aec485820edfa064ftree | snapshot
parent11d81280208345b189c174e2ae19a6ab45e2b03acommit | diff
added new extractor based on MetadataDb.index_obj
helm/ocaml/metadata/Makefile diff | blob | history
helm/ocaml/metadata/extractor/Makefile [new file with mode: 0644] blob
helm/ocaml/metadata/extractor/extractor.conf.xml [new file with mode: 0644] blob
helm/ocaml/metadata/extractor/extractor.ml [new file with mode: 0644] blob
Unnamed repository; edit this file 'description' to name the repository.