]> matita.cs.unibo.it Git - helm.git/commit
added "unindex" to undo indexing of a single object
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 10 Feb 2005 15:51:42 +0000 (15:51 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 10 Feb 2005 15:51:42 +0000 (15:51 +0000)
commitdf29cafb872244de1a6a9b3c273b329a6e15fa8c
treec8fbe0bb9bfd9e0e8d591a6a34e46bc7bdc7085f
parentf264827750988795bd85d0eb6a7d3ecf236d224e
added "unindex" to undo indexing of a single object
helm/ocaml/metadata/metadataDb.ml
helm/ocaml/metadata/metadataDb.mli