]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/matitaScript.ml
Dead code removed.
[helm.git] / matita / matita / matitaScript.ml
index 8ed2fa910b9fa7cf482a2e1f8772ed429809b867..1f05a8837e1e5ecf95fe548839ade424960c73a6 100644 (file)
@@ -835,11 +835,6 @@ object (self)
   method activate =
     self#notify
 
-  method loadFromString s =
-    buffer#set_text s;
-    self#reset_buffer;
-    buffer#set_modified true
-
   method loadFromFile f =
     buffer#set_text (HExtlib.input_file f);
     self#reset_buffer;