]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 56bf133) | patch
MetadataDB.clean now cleans the getter maps (calling Http_getter.unregister)
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 1 Feb 2005 13:44:27 +0000 (13:44 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 1 Feb 2005 13:44:27 +0000 (13:44 +0000)
commit9eb303488eea42ec9cd1f588f49b293148878a37
tree84e477e7dffe3b86a8f0339e93a34819a4a5f4dbtree | snapshot
parent56bf133e9df9c7b689e0c3059fffdc1f8736a936commit | diff
MetadataDB.clean now cleans the getter maps (calling Http_getter.unregister)
from the uris that deletes from the DB
helm/ocaml/metadata/metadataDb.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.