From 088377896f207fac6f53c4e4d43df1cb3b7a9589 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 9 Jun 2005 11:46:28 +0000 Subject: [PATCH] added \n to "file saved" message --- helm/matita/matitaGui.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 08f097086..34238f80d 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -183,7 +183,7 @@ class gui () = match self#chooseFile ~ok_not_exists:true () with | Some f -> script#saveTo f; - console#message ("'"^f^"' saved."); + console#message ("'"^f^"' saved.\n"); self#_enableSaveTo f | None -> () in @@ -192,7 +192,7 @@ class gui () = | None -> saveAsScript () | Some f -> (s ())#saveTo f; - console#message ("'"^f^"' saved."); + console#message ("'"^f^"' saved.\n"); in let newScript () = (s ())#reset (); disableSave () in let cursor () = -- 2.39.2