]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1c0aa5a) | patch
do not share the db connection among children, should fix the "server has gone away...
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 5 Dec 2006 13:30:22 +0000 (13:30 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 5 Dec 2006 13:30:22 +0000 (13:30 +0000)
commite98e464e933174ad6577596d32cba1de758ea919
tree7e50b183e35c12459dd87e72eac6647d5cf3ce1atree | snapshot
parent1c0aa5a6fe9b54787046c7e0270760ad197ee460commit | diff
do not share the db connection among children, should fix the "server has gone away" error
daemons/whelp/searchEngine.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.