diff options
Diffstat (limited to 'tools/coq_makefile.ml')
| -rw-r--r-- | tools/coq_makefile.ml | 1 |
1 files changed, 1 insertions, 0 deletions
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 |