diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/tags.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/tags.ml b/ide/tags.ml index 556430aafc..cc615d9e15 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -20,7 +20,7 @@ module Script = struct let table = GText.tag_table () let comment = make_tag table ~name:"comment" [] - let error = make_tag table ~name:"error" [`UNDERLINE `DOUBLE ; `FOREGROUND "red"] + let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE ; `FOREGROUND "red"] let error_bg = make_tag table ~name:"error_bg" [`BACKGROUND "#FFCCCC"] let to_process = make_tag table ~name:"to_process" [`BACKGROUND !processing_color] let processed = make_tag table ~name:"processed" [`BACKGROUND !processed_color] |