aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-10-12 21:54:05 +0200
committerPierre-Marie Pédrot2016-10-12 21:54:05 +0200
commit376b54ff8753496a54fb120e35cd1b8babb44ac9 (patch)
treeb55be0ecb60aae1a413fd7b275ccf8e32a76f1ca /toplevel
parentd873f82c5024a496e8f1a14a9839e7f377d5f4bb (diff)
parente1f25889f88e078dac0f3b454eb16a470dd5f9ae (diff)
Merge PR #224 into v8.6
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/coqtop.ml6
1 files changed, 2 insertions, 4 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index ebdf804ba0..7a67e0951f 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -61,8 +61,7 @@ let init_color () =
match colors with
| None ->
(** Default colors *)
- Ppstyle.init_color_output ();
- Feedback.set_logger Feedback.color_terminal_logger
+ Feedback.init_color_output ()
| Some "" ->
(** No color output *)
()
@@ -70,8 +69,7 @@ let init_color () =
(** Overwrite all colors *)
Ppstyle.clear_styles ();
Ppstyle.parse_config s;
- Ppstyle.init_color_output ();
- Feedback.set_logger Feedback.color_terminal_logger
+ Feedback.init_color_output ()
end
let toploop_init = ref begin fun x ->