diff options
| author | Enrico Tassi | 2013-11-27 15:06:53 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2013-11-27 15:12:06 +0100 |
| commit | f8968fb29a3fc4032622e4ebfb68be75d1c97c58 (patch) | |
| tree | 86816774a6dd33dd43c797a61450c66e7b102acf /kernel | |
| parent | c48d806ab20951916ed5a7062eabef440f314fbe (diff) | |
STM: restart slave after every proof
The code now passes a cleanup function that, if slave is not
killed, could be used to do some cleanup between two jobs.
ATM I don't know how to reuse the worker without having it
grow in space indefinitely. Running Gc.compact is too expensive.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions