diff options
| author | Hugo Herbelin | 2017-10-22 21:59:16 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-10-22 22:32:46 +0200 |
| commit | d651d81a13d78f0466d2a08c06e7f2318c42da5f (patch) | |
| tree | c0b3d2f37232bd1613a6ef3c20fd3430a9cb6577 /kernel/nativelambda.mli | |
| parent | 0897d0f642c19419c513f9609782436bebf28f5b (diff) | |
An attempt to fix issue #5771 (error color hidden by warning color).
We change the relative priority of errors and warnings, so that the
error takes precedence.
It is unsure that it is universally the best choice. If the location
of the error is finer than the one of the warning, it is better. In
the other way round, it might be less good, e.g. if understanding the
warning helps to understand the error.
Maybe the best policy would be to test the relative locations of the
warning and error?
Trying to consider the error as more important, at the current time.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions
