]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: de49318) | 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)
commit482b253669956d149dd6edd06d5421915f27b6c1
treef9f92e457409e1735e50c94c43757f8e77ce4a01tree | snapshot
parentde49318d8e44cfcba7215f0981afdc7ab4c16473commit | diff
do not share the db connection among children, should fix the "server has gone away" error
helm/software/daemons/whelp/searchEngine.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.