aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/coqProject_file.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'lib/coqProject_file.ml4')
-rw-r--r--lib/coqProject_file.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
index 1e52af0be..e6f1d7e06 100644
--- a/lib/coqProject_file.ml4
+++ b/lib/coqProject_file.ml4
@@ -114,7 +114,7 @@ let process_cmd_line orig_dir proj args =
let parsing_project_file = ref (proj.project_file <> None) in
let orig_dir = (* avoids turning foo.v in ./foo.v *)
if orig_dir = "." then "" else orig_dir in
- let error s = Feedback.msg_error (Pp.str (s^".")); exit 1 in
+ let error s = Format.eprintf "@[%a]@@\n%!" Pp.pp_with Pp.(str (s^".")); exit 1 in
let mk_path d =
let p = CUnix.correct_path d orig_dir in
{ path = CUnix.remove_path_dot (post_canonize p);