aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/tags.mli
diff options
context:
space:
mode:
Diffstat (limited to 'ide/tags.mli')
-rw-r--r--ide/tags.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/tags.mli b/ide/tags.mli
index d86dcbc44..ddd240d2a 100644
--- a/ide/tags.mli
+++ b/ide/tags.mli
@@ -11,6 +11,7 @@ sig
val table : GText.tag_table
val comment_sentence : GText.tag
val error : GText.tag
+ val error_bg : GText.tag
val to_process : GText.tag
val processed : GText.tag
val unjustified : GText.tag