diff options
| author | Pierre-Marie Pédrot | 2014-03-28 13:32:11 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-03-28 13:32:11 +0100 |
| commit | 8934da82d30fee8205fe1694ed601817ff858e5c (patch) | |
| tree | f8a3b93a64b6537c6c2c723655e9dde69b49b82d | |
| parent | dcd6f0076ba940f606083ae8836dc05df398c956 (diff) | |
Newline on -slash warning in coqdep.
| -rw-r--r-- | tools/coqdep.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 17e56bc63b..ea5eb02c12 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -463,7 +463,7 @@ let rec parse = function | "-suffix" :: s :: ll -> suffixe := s ; parse ll | "-suffix" :: [] -> usage () | "-slash" :: ll -> - Printf.eprintf "warning: option -slash has no effect and is deprecated."; + Printf.eprintf "warning: option -slash has no effect and is deprecated.\n"; parse ll | ("-h"|"--help"|"-help") :: _ -> usage () | f :: ll -> treat_file None f; parse ll |