diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/check.ml | 2 | ||||
| -rw-r--r-- | checker/check.mllib | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/checker/check.ml b/checker/check.ml index 267fdb886a..0d8a4cd222 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -177,7 +177,7 @@ let add_load_path (phys_path,coq_path) = begin (* Assume the user is concerned by library naming *) if dir <> default_root_prefix then - Flags.if_warn msg_warning + msg_warning (str phys_path ++ strbrk " was previously bound to " ++ pr_dirpath dir ++ strbrk "; it is remapped to " ++ pr_dirpath coq_path); diff --git a/checker/check.mllib b/checker/check.mllib index 2671788b4c..48c6290096 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -4,8 +4,8 @@ Option Store Exninfo Backtrace -Pp_control Flags +Pp_control Pp Loc Segmenttree |