]> matita.cs.unibo.it Git - helm.git/commit
Quick&dirty patch to make Http_getter_storage.is_empty ignore {.moo,.metadata.lexicon...
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 18 Jul 2006 13:57:43 +0000 (13:57 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 18 Jul 2006 13:57:43 +0000 (13:57 +0000)
commit9052c3d19ade20c086bb114133fe7cd060e23ec4
tree349d28a269916e10aced559bb77eda77beda795e
parent27be353376ced722d0a8d25078a7361d12fffae3
Quick&dirty patch to make Http_getter_storage.is_empty ignore {.moo,.metadata.lexicon} files.
helm/software/components/getter/http_getter_storage.ml