diff options
Diffstat (limited to 'ide/tags.ml')
| -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 89adad2c1..b0b9dc6fb 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -38,7 +38,7 @@ struct let hypothesis = make_tag table ~name:"hypothesis" [] let goal = make_tag table ~name:"goal" [] end -module Message = +module Message = struct let table = GText.tag_table () let error = make_tag table ~name:"error" [`FOREGROUND "red"] |