• Sylvain Dailler's avatar
    ide: Use a different color on parsing error · 8ed7c5ec
    Sylvain Dailler authored
    By default, the color used for font errors in the messages view is used
    as background for precise locations of errors in source.
    Perhaps, its a good idea to change the color in the future.
    8ed7c5ec
itp_communication.ml 8.63 KB