aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/coqdep.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 2433cb1d0..ca14b11bc 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -539,4 +539,4 @@ let _ =
coqdep ()
with CErrors.UserError(s,p) ->
let pp = (match s with | None -> p | Some s -> Pp.(str s ++ str ": " ++ p)) in
- Feedback.msg_error pp
+ Format.eprintf "%a@\n%!" Pp.pp_with pp