diff options
| author | Emilio Jesus Gallego Arias | 2017-03-22 23:23:14 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-03-24 13:14:59 +0100 |
| commit | 43ac25fd5218fb92b3971c8df8be4f38894e27f3 (patch) | |
| tree | 03f1da9560f09a0c04d4c2823ae30b8459988556 /toplevel | |
| parent | 530cd175c1b7465c3fa35c300f42b022bed9b25b (diff) | |
[nit] Fix a couple incorrect uses of msg_error.
Diffstat (limited to 'toplevel')
| -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 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 |
