diff options
| author | Pierre-Marie Pédrot | 2015-02-12 22:07:32 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-12 23:01:36 +0100 |
| commit | 69212fa135879b8df4cf3347a6bee0af769a3ee7 (patch) | |
| tree | 3c4a90f9746804c7c910c5bc7362c68552ea43ea /kernel/type_errors.mli | |
| 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 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions