diff options
| author | Emilio Jesus Gallego Arias | 2017-04-08 18:00:49 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-04-08 18:16:30 +0200 |
| commit | de8b0d5d60b3b9b59cafc32f491aa16d4924b9ac (patch) | |
| tree | 10e168a805df5b2fec0c800fb8624f2e7e0e7f11 /kernel/nativecode.ml | |
| parent | 2c0287fe8445bd4b599bf8498bcb71b2a7df0d51 (diff) | |
[ide] Correctly place warning tags.
8e07227c5853de78eaed4577eefe908fb84507c0 introduced an
incorrect duplicate of `position_error_tag_at_sentence`, which
sets the end of the underlining position starting at the end of the
sentence, whereas the location in the feedback refers to the
beginning, thus it highlights more text than it should.
This was missed in 8.6 as it seems that the code was not called.
We undo the duplication and fix the bug.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions