aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2017-03-22 23:23:14 +0100
committerEmilio Jesus Gallego Arias2017-03-24 13:14:59 +0100
commit43ac25fd5218fb92b3971c8df8be4f38894e27f3 (patch)
tree03f1da9560f09a0c04d4c2823ae30b8459988556 /toplevel
parent530cd175c1b7465c3fa35c300f42b022bed9b25b (diff)
[nit] Fix a couple incorrect uses of msg_error.
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/vernac.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 06908abb6e..9917a49b42 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -266,9 +266,9 @@ let ensure_bname src tgt =
let src, tgt = Filename.basename src, Filename.basename tgt in
let src, tgt = chop_extension src, chop_extension tgt in
if src <> tgt then begin
- Feedback.msg_error (str "Source and target file names must coincide, directories can differ");
- Feedback.msg_error (str "Source: " ++ str src);
- Feedback.msg_error (str "Target: " ++ str tgt);
+ Feedback.msg_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++
+ str "Source: " ++ str src ++ fnl () ++
+ str "Target: " ++ str tgt);
flush_all ();
exit 1
end