diff options
Diffstat (limited to 'toplevel/vernac.ml')
| -rw-r--r-- | toplevel/vernac.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 06908abb6..9917a49b4 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 |