]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e9aaf3f) | patch
- cathes more Mysql errors which could happen during post-indexing actions
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 17 May 2005 13:05:38 +0000 (13:05 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 17 May 2005 13:05:38 +0000 (13:05 +0000)
commit728c74fc32dc03e9ffde18ac060dcdef3ca55de9
tree684f7f9ec07afcc68d19c75d176f132e5ac62f77tree | snapshot
parente9aaf3fb77afbe96c033ce2940734edd8f2cde88commit | diff
- cathes more Mysql errors which could happen during post-indexing actions
- bugfix in hits table handling during post-indexing actions
- added copyright info
helm/ocaml/metadata/extractor/extractor_manager.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.