diff options
Diffstat (limited to 'toplevel/mltop.ml4')
| -rw-r--r-- | toplevel/mltop.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 3cda90425..ff3ce8a09 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -143,8 +143,8 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = let convert_string d = try Names.id_of_string d with _ -> - if_verbose warning - ("Directory "^d^" cannot be used as a Coq identifier (skipped)"); + if_warn msg_warning + (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)")); flush_all (); failwith "caught" |