aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorHugo Herbelin2017-10-22 21:59:16 +0200
committerHugo Herbelin2017-10-22 22:32:46 +0200
commitd651d81a13d78f0466d2a08c06e7f2318c42da5f (patch)
treec0b3d2f37232bd1613a6ef3c20fd3430a9cb6577 /dev
parent0897d0f642c19419c513f9609782436bebf28f5b (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 'dev')
0 files changed, 0 insertions, 0 deletions