diff options
| author | Emilio Jesus Gallego Arias | 2018-04-01 02:57:02 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-04-01 03:11:21 +0200 |
| commit | 0b48c57d705873d142cb4b19f959d1e7fab116c8 (patch) | |
| tree | 312b59fdae50e463c80e563783c93bb0013957db /dev/ci/ci-iris-lambda-rust.sh | |
| parent | 2d2d16430822f1768ce4f3c62ef0750b94e4747f (diff) | |
[toplevel] Protect goal printing better wrt Break [fixes #7142]
When interrupting goal printing, we should continue the loop with the
newly generated state, that should help avoiding synchronization
problems as in #7142.
Fixes #7142.
Diffstat (limited to 'dev/ci/ci-iris-lambda-rust.sh')
0 files changed, 0 insertions, 0 deletions