aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/printmod.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/printmod.ml')
-rw-r--r--printing/printmod.ml10
1 files changed, 4 insertions, 6 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 521b4ec2a..baa1b8d79 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -28,12 +28,10 @@ open Goptions
module Tag =
struct
- let definition =
- let style = Terminal.make ~bold:true ~fg_color:`LIGHT_RED () in
- Ppstyle.make ~style ["module"; "definition"]
- let keyword =
- let style = Terminal.make ~bold:true () in
- Ppstyle.make ~style ["module"; "keyword"]
+
+ let definition = "module.definition"
+ let keyword = "module.keyword"
+
end
let tag t s = Pp.tag t s