From b455e96cce263ea48ff0aa8b8ebf530d0f1eea9c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Mon, 6 Nov 2017 21:09:00 +0100
Subject: Registering a printing handler in coq_makefile.

This allows to fix the non-printing of error messages produced when
parsing arguments.
---
 tools/coq_makefile.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'tools/coq_makefile.ml')

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index ee59479a5..b7a62a78c 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -391,6 +391,7 @@ let share_prefix s1 s2 =
   | _ -> false
 
 let _ =
+  let _fhandle = Feedback.(add_feeder (console_feedback_listener Format.err_formatter)) in
   let prog, args =
     let args = Array.to_list Sys.argv in
     let prog = List.hd args in
-- 
cgit v1.2.3