diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-18 04:47:38 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-18 04:48:27 +0200 |
| commit | 6ef8a007e77c61d9f8c2b19b19dc22548f1896ca (patch) | |
| tree | 28b289f8422b435b7ae5ca55c7725f6a1a4a1f45 /kernel/entries.mli | |
| parent | 6d770156669dd9868ae7623b8f4302866e2cc8c7 (diff) | |
[toplevel] [stm] Avoid edit_at in batch mode (bug #5520)
In non-interactive mode, `edit_at` seems to do very weird things, for
instance will try to recompute all the previous states which seems
weird.
We better avoid that to approximate 8.6 behavior while we investigate
more.
Diffstat (limited to 'kernel/entries.mli')
0 files changed, 0 insertions, 0 deletions