]> 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)
commit15e240ca94dbca536121c9da942851fcaae951f9
treeb5612e798fb763fd446200bb62f8c669f36ecf21
parentb65592962c5614981b20154000779805c3620075
Quick&dirty patch to make Http_getter_storage.is_empty ignore {.moo,.metadata.lexicon} files.
components/getter/http_getter_storage.ml