From a33f7ad548ed312a2665c87baca9fb7b233e8cbf Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 20 Apr 2015 16:20:40 +0200
Subject: Remove spurious ".v" from warning message.

---
 tools/coqdep_common.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 2e6a15cebd..d86e05d8cf 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -136,10 +136,8 @@ let error_cannot_parse s (i,j) =
   exit 1
 
 let warning_module_notfound f s =
-  eprintf "*** Warning: in file %s, library " f;
-  eprintf "%s.v is required and has not been found in the loadpath!\n"
-    (String.concat "." s);
-  flush stderr
+  eprintf "*** Warning: in file %s, library %s is required and has not been found in the loadpath!\n%!"
+    f (String.concat "." s)
 
 let warning_notfound f s =
   eprintf "*** Warning: in file %s, the file " f;
-- 
cgit v1.2.3