diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-01 02:57:02 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-01 03:11:21 +0200 |
| commit | 0b48c57d705873d142cb4b19f959d1e7fab116c8 (patch) | |
| tree | 312b59fdae50e463c80e563783c93bb0013957db /plugins/ssr | |
| 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 'plugins/ssr')
0 files changed, 0 insertions, 0 deletions