diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-05-09 14:46:11 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-05-09 14:46:11 +0200 |
| commit | 213e86842db2cdc3acc8cdf6d28f46c7ebaec5d4 (patch) | |
| tree | 1e9bb531e72906cd3792f9a6bbca88acd5ade9e8 /toplevel/vernacentries.mli | |
| parent | 4422432dd55c823595f31163c92306349769d3e4 (diff) | |
Use the actual location of an error in the error pane (bug #4169).
A "sentence" includes all the blank lines and all the comments that
precede a command. So its starting location might be far from any error it
contains. This patch changes error reporting so that it relies on the
location of errors rather than the location of erroneous sentences.
Diffstat (limited to 'toplevel/vernacentries.mli')
0 files changed, 0 insertions, 0 deletions