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 /ide/ide_slave.ml | |
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 'ide/ide_slave.ml')
0 files changed, 0 insertions, 0 deletions