From 43ac25fd5218fb92b3971c8df8be4f38894e27f3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 22 Mar 2017 23:23:14 +0100
Subject: [nit] Fix a couple incorrect uses of msg_error.

---
 toplevel/vernac.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'toplevel')

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
-- 
cgit v1.2.3