]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 909cdbb) | patch
Exceptions should never escape the final exception handler for the worker
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 9 Feb 2007 15:12:07 +0000 (15:12 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 9 Feb 2007 15:12:07 +0000 (15:12 +0000)
commitb36c499a9234a3dc0abd5fb8d418975966f179e7
treed2902998ce7fd49ff27a1b227dc09bad486d7b8atree | snapshot
parent909cdbb5ddf942e75558149c9f11819c6c84bc3acommit | diff
Exceptions should never escape the final exception handler for the worker
threads. This patch just reduces the probability.
matita/matitaGui.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.