When matita is started on a non-existent file, it avoids creating it

[helm.git] / helm / matita / matitaScript.ml

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index f339ebb40f3547756b9349666d1637408b98371d..ad1530d4ea15220171ec175aa0eebb1cc7e108f4 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -542,8 +542,8 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
     let status = self#status in
     List.iter (fun o -> o status) observers
 
-  method loadFromFile () =
-    buffer#set_text (MatitaMisc.input_file self#getFilename);
+  method loadFromFile f =
+    buffer#set_text (MatitaMisc.input_file f);
     self#goto_top;
     buffer#set_modified false