aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorvgross2009-12-07 16:55:21 +0000
committervgross2009-12-07 16:55:21 +0000
commit2f0e6e0a89babb9c4ee4e513d6cbd6de2f858a3a (patch)
tree10d4ccf233a234660074c798cedaac355b2f8312
parent8f4d0165f0a1be1b81ecab0356f7040423406c28 (diff)
Fix bug #2197 (option show_toolbar not taken into account at startup)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12568 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--ide/coqide.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 99b2593087..fe71784b32 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -3436,6 +3436,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
activate_input index;
end;
initial_about session_notebook#current_term.proof_view#buffer;
+ !show_toolbar !current.show_toolbar;
session_notebook#current_term.script#misc#grab_focus ()
;;