mirror of
https://github.com/paparazzi/paparazzi.git
synced 2026-06-01 12:57:27 +08:00
paparazzicenter: green background color for info messages (e.g. via #pragma message)
This commit is contained in:
@@ -206,7 +206,8 @@ let () =
|
||||
gui#console#set_buffer buffer;
|
||||
|
||||
let errors = "red", ["error"; "no such file"; "undefined reference"; "failure"]
|
||||
and warnings = "orange", ["warning"] in
|
||||
and warnings = "orange", ["warning"]
|
||||
and info = "green", ["message"; "info"] in
|
||||
|
||||
let color_regexps =
|
||||
List.map (fun (color, strings) ->
|
||||
@@ -214,7 +215,7 @@ let () =
|
||||
let s = String.concat "\\|" s in
|
||||
let s = ".*\\("^s^"\\)" in
|
||||
color, Str.regexp_case_fold s)
|
||||
[errors; warnings] in
|
||||
[errors; warnings; info] in
|
||||
let compute_tags = fun s ->
|
||||
let rec loop = function
|
||||
(color, regexp)::rs ->
|
||||
|
||||
Reference in New Issue
Block a user