fixed a problem when newScript was called

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index c3e169c50a371c39051cc7b9863484cfc2f00053..540a839ddd99fec4fc09f04b1ee82875aa395c2d 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -292,7 +292,8 @@ class gui () =
       let newScript () = 
         (s ())#reset (); 
         (s ())#template (); 
-        disableSave () 
+        disableSave ();
+        script_fname <- None
       in
       let cursor () =
         source_buffer#place_cursor