]> matita.cs.unibo.it Git - helm.git/commitdiff
added \n to "file saved" message
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 9 Jun 2005 11:46:28 +0000 (11:46 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 9 Jun 2005 11:46:28 +0000 (11:46 +0000)
helm/matita/matitaGui.ml

index 08f097086fdc59540b7c9c683f3a6cf8d27b62f7..34238f80d4e66cb199d7c0f232f4b6dfb0c29f65 100644 (file)
@@ -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 () =