snapshot, notably:

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

diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml
index 5fb44adf486511c92067e5fd595c5c3cd0faa94e..603a480f45553392920cf27e3c67a031b1d80453 100644 (file)
--- a/helm/matita/matitaConsole.ml
+++ b/helm/matita/matitaConsole.ml
@@ -165,7 +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#lock;
+      self#echo_prompt ()
 
       (** navigation methods: history, cursor motion, ... *)