diff options
| author | Hugo Herbelin | 2020-06-01 17:39:47 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2021-04-06 17:40:53 +0200 |
| commit | 2ee505630756676ded9f8eb6511ad642c80179ee (patch) | |
| tree | 0fa3f7ec475ee5e8412e63caf5a412f8656ac7af /library/lib.ml | |
| parent | 524eb4e7dcb18d622ebb99648862e5d08a972117 (diff) | |
Uniformizing the "already exists" messages
Diffstat (limited to 'library/lib.ml')
| -rw-r--r-- | library/lib.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/lib.ml b/library/lib.ml index fa0a95d366..3172511c26 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -280,7 +280,7 @@ let start_mod is_type export id mp fs = else Nametab.exists_dir dir in if exists then - user_err ~hdr:"open_module" (Id.print id ++ str " already exists"); + user_err ~hdr:"open_module" (Id.print id ++ str " already exists."); add_entry (make_foname id) (OpenedModule (is_type,export,prefix,fs)); lib_state := { !lib_state with path_prefix = prefix} ; prefix |