snapshot, notably:

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

diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml
index 2f36fc647a065479bf6c553f6a4cfbdf1dcd557c..3d40e949ee46ae156abe5e34625c7dbac8346fc2 100644 (file)
--- a/helm/matita/matitaConsole.ml
+++ b/helm/matita/matitaConsole.ml
@@ -198,8 +198,10 @@ class console
       self#buffer#insert msg;
       paned#set_position (self#get_max_position - console_height);
       self#misc#grab_focus ()
-    method hide () =
-      paned#set_position self#get_max_position
+    method hide () =  (* ZACK still not sure about the gui, for the moment just
+                       * keep the console persistent *)
+      ()
+(*       paned#set_position self#get_max_position *)
     method toggle () =
       let pos = self#get_position in
       if pos > self#get_max_position - console_height then