aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep_common.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdep_common.ml')
-rw-r--r--tools/coqdep_common.ml6
1 files changed, 2 insertions, 4 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 2e6a15ceb..d86e05d8c 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;