From 2ee505630756676ded9f8eb6511ad642c80179ee Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 1 Jun 2020 17:39:47 +0200
Subject: Uniformizing the "already exists" messages

---
 library/lib.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library/lib.ml')

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
-- 
cgit v1.2.3