snapshot, notably:

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

diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml
index 603a480f45553392920cf27e3c67a031b1d80453..eb77ffa5d62ac8f95bac2b34ff198cd438f8ceaf 100644 (file)
--- a/helm/matita/matitaConsole.ml
+++ b/helm/matita/matitaConsole.ml
@@ -165,8 +165,8 @@ class console
       buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag error_props]
         (msg ^ "\n");
       self#ignore_insert_text_signal false;
-      self#lock;
-      self#echo_prompt ()
+      self#lock
+(*       self#echo_prompt () *)
 
       (** navigation methods: history, cursor motion, ... *)