diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-04-20 16:20:40 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-04-20 16:20:40 +0200 |
| commit | a33f7ad548ed312a2665c87baca9fb7b233e8cbf (patch) | |
| tree | 9e163b6d982ba7aeda6fed85a4b69553f1377ffe /tools/coqdep_common.ml | |
| parent | 94afd8996251c30d2188a75934487009538e1303 (diff) | |
Remove spurious ".v" from warning message.
Diffstat (limited to 'tools/coqdep_common.ml')
| -rw-r--r-- | tools/coqdep_common.ml | 6 |
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; |