diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-12 22:07:32 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-12 23:01:36 +0100 |
| commit | 69212fa135879b8df4cf3347a6bee0af769a3ee7 (patch) | |
| tree | 3c4a90f9746804c7c910c5bc7362c68552ea43ea /ide/session.ml | |
| parent | 1e1a2f1803c57cc1697e294a7610b76a95661687 (diff) | |
Tentative fix for CoqIDE randomly dropping deletions.
We make the deletion callback not to regenerate a task id, as the insertion
callback does. I can't find a particular reason for this dissymetry, and it
was indeed causing trouble.
Diffstat (limited to 'ide/session.ml')
| -rw-r--r-- | ide/session.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/ide/session.ml b/ide/session.ml index 072ae61c6..47b747dae 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -160,7 +160,6 @@ let set_buffer_handlers end end in let delete_cb ~start ~stop = Minilib.log (Printf.sprintf "delete_cb %d %d" start#offset stop#offset); - cur_action := new_action_id (); let min_iter, max_iter = if start#compare stop < 0 then start, stop else stop, start in let text_mark = add_mark min_iter in |