snapshot

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 0d46bfcfaf621f44fde9f30e9c0650d906f672f3..26cf9df086cacdd54511d0ded7bb5dab02fa40b0 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -89,7 +89,7 @@ class gui file =
             toggle_win ~check:main#showCheckMenuItem check#checkWin;
           GdkKeysyms._F5,
             toggle_win ~check:main#showScriptMenuItem script#scriptWin;
-          GdkKeysyms._x, (fun () -> console#show ());
+          GdkKeysyms._x, (fun () -> console#toggle ());
         ];
         (* about win *)
       ignore (about#aboutWin#event#connect#delete (fun _ -> true));
@@ -123,7 +123,7 @@ class gui file =
       List.iter (fun w -> w#misc#set_sensitive false)
         [ main#saveMenuItem; main#saveAsMenuItem ];
       main#helpMenu#set_right_justified true;
-      ignore (main#showConsoleMenuItem#connect#activate console#show);
+      ignore (main#showConsoleMenuItem#connect#activate console#toggle);
         (* main *)
       connect_button main#hideConsoleButton console#hide;
 (*