diff options
| author | Enrico Tassi | 2019-02-11 16:07:59 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-02-11 16:10:46 +0100 |
| commit | 7832bb5071c7ce21ca285e86b288488b3dfe3e86 (patch) | |
| tree | 8d2a276c4872b6fc5e2116eba17bf8b2d40ccdfa /kernel/reduction.ml | |
| parent | 30a8190264267e0567f6c52ed263cb4fb6ac9b0c (diff) | |
[ide] fix unconditional goto-point on editing an error (fix #9488)
Diffstat (limited to 'kernel/reduction.ml')
0 files changed, 0 insertions, 0 deletions